10 val ttt = (term_of o the o (parseold thy)) |
10 val ttt = (term_of o the o (parseold thy)) |
11 "Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_e"; |
11 "Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_e"; |
12 |
12 |
13 val ttt = (term_of o the o (parse thy)) |
13 val ttt = (term_of o the o (parse thy)) |
14 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
14 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
15 \[e_]"; |
15 \[e_e]"; |
16 val ttt = (term_of o the o (parse thy)) |
16 val ttt = (term_of o the o (parse thy)) |
17 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
17 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
18 \((%e_. [e_]) e_e)"; |
18 \((%e_. [e_e]) e_e)"; |
19 val ttt = (term_of o the o (parse thy)) |
19 val ttt = (term_of o the o (parse thy)) |
20 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
20 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
21 \((%e_. (let e_e = e_e in [e_])) e_e)"; |
21 \((%e_. (let e_e = e_e in [e_e])) e_e)"; |
22 val ttt = (term_of o the o (parse thy)) |
22 val ttt = (term_of o the o (parse thy)) |
23 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
23 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
24 \((%e_. \ |
24 \((%e_. \ |
25 \ (let e_e = ((Rewrite_Set SqRoot_simplify False) e_e)\ |
25 \ (let e_e = ((Rewrite_Set SqRoot_simplify False) e_e)\ |
26 \ in [e_]))\ |
26 \ in [e_e]))\ |
27 \ e_e)"; |
27 \ e_e)"; |
28 val ttt = (term_of o the o (parse thy)) |
28 val ttt = (term_of o the o (parse thy)) |
29 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
29 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
30 \((%ee_. (let e_e = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_])) e_e)"; |
30 \((%ee_. (let e_e = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_e])) e_e)"; |
31 |
31 |
32 val ttt = (term_of o the o (parse thy)) |
32 val ttt = (term_of o the o (parse thy)) |
33 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
33 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
34 \(let e_e = \ |
34 \(let e_e = \ |
35 \ (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\ |
35 \ (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\ |
36 \ in [e_])"; |
36 \ in [e_e])"; |
37 (*----*) |
37 (*----*) |
38 val ttt = (term_of o the o (parse thy)) |
38 val ttt = (term_of o the o (parse thy)) |
39 |
39 |
40 (*----*) |
40 (*----*) |
41 val ttt = (term_of o the o (parse thy)) |
41 val ttt = (term_of o the o (parse thy)) |
43 \(let e_e = \ |
43 \(let e_e = \ |
44 \ (Repeat\ |
44 \ (Repeat\ |
45 \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\ |
45 \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\ |
46 \ e_e)\ |
46 \ e_e)\ |
47 \ e_e)\ |
47 \ e_e)\ |
48 \ in [e_])"; |
48 \ in [e_e])"; |
49 val ttt = (term_of o the o (parse thy)) |
49 val ttt = (term_of o the o (parse thy)) |
50 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
50 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
51 \(let e_e = \ |
51 \(let e_e = \ |
52 \ (Repeat\ |
52 \ (Repeat\ |
53 \ ((%ee_.\ |
53 \ ((%ee_.\ |
54 \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\ |
54 \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\ |
55 \ e_e)\ |
55 \ e_e)\ |
56 \ e_e)\ |
56 \ e_e)\ |
57 \ in [e_])"; |
57 \ in [e_e])"; |
58 val ttt = (term_of o the o (parse thy)) |
58 val ttt = (term_of o the o (parse thy)) |
59 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
59 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
60 \(let e_e = \ |
60 \(let e_e = \ |
61 \ (Repeat\ |
61 \ (Repeat\ |
62 \ ((%ee_.\ |
62 \ ((%ee_.\ |
63 \ (let e_e = ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\ |
63 \ (let e_e = ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\ |
64 \ in ((Rewrite_Set SqRoot_simplify False) e_e)) )\ |
64 \ in ((Rewrite_Set SqRoot_simplify False) e_e)) )\ |
65 \ e_e)\ |
65 \ e_e)\ |
66 \ e_e)\ |
66 \ e_e)\ |
67 \ in [e_])"; |
67 \ in [e_e])"; |
68 atomty ttt; |
68 atomty ttt; |
69 atomt ttt; |
69 atomt ttt; |
70 |
70 |
71 val ttt = (term_of o the o (parse thy)) |
71 val ttt = (term_of o the o (parse thy)) |
72 "Script Testterm (g_::real) = \ |
72 "Script Testterm (g_::real) = \ |
121 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
121 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
122 \(let e_e = \ |
122 \(let e_e = \ |
123 \ ((Repeat\ |
123 \ ((Repeat\ |
124 \ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\ |
124 \ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\ |
125 \ (Rewrite_Set SqRoot_simplify False)))) e_e)\ |
125 \ (Rewrite_Set SqRoot_simplify False)))) e_e)\ |
126 \ in [e_])"; |
126 \ in [e_e])"; |
127 atomty ttt; |
127 atomty ttt; |
128 |
128 |
129 |
129 |
130 val ttt = (term_of o the o (parse thy)) |
130 val ttt = (term_of o the o (parse thy)) |
131 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy"; |
131 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy"; |