13 "-----------------------------------------------------------------"; |
13 "-----------------------------------------------------------------"; |
14 "-----------------------------------------------------------------"; |
14 "-----------------------------------------------------------------"; |
15 "-----------------------------------------------------------------"; |
15 "-----------------------------------------------------------------"; |
16 |
16 |
17 val thy = @{theory "AlgEin"}; |
17 val thy = @{theory "AlgEin"}; |
18 |
18 val ctxt = Proof_Context.init_global thy; |
19 |
|
20 (* use"../smltest/IsacKnowledge/algein.sml"; |
|
21 *) |
|
22 |
19 |
23 "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; |
20 "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; |
24 "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; |
21 "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; |
25 "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; |
22 "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; |
26 val str = |
23 val str = |
27 "Program RechnenSymbolScript (k_k::bool) (q__q::bool) \ |
24 "Program RechnenSymbolScript (k_k::bool) (q__q::bool) \ |
28 \(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\ |
25 \(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\ |
29 \ (let t_t = (l_l = 1)\ |
26 \ (let t_t = (l_l = 1)\ |
30 \ in t_t)" |
27 \ in t_t)" |
31 ; |
28 ; |
32 val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; |
29 val sc = (inst_abs o (TermC.parseNEW' ctxt)) str; |
33 TermC.atomty sc; |
30 TermC.atomty sc; |
34 atomt sc; |
31 atomt sc; |
35 |
32 |
36 "----------- me 'Berechnung' 'erstNumerisch' ---------------------"; |
33 "----------- me 'Berechnung' 'erstNumerisch' ---------------------"; |
37 "----------- me 'Berechnung' 'erstNumerisch' ---------------------"; |
34 "----------- me 'Berechnung' 'erstNumerisch' ---------------------"; |