1 val ttt = (term_of o the o (parse thy)) |
1 val ttt = (term_of o the o (parse thy)) |
2 "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_e"; |
2 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e"; |
3 val ttt = (term_of o the o (parse thy)) |
3 val ttt = (term_of o the o (parse thy)) |
4 "(Try (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_e)"; |
4 "(Try (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e)"; |
5 |
5 |
6 val ttt = (term_of o the o (parse thy)) |
6 val ttt = (term_of o the o (parse thy)) |
7 "(Rewrite_Set SqRoot_simplify False) e_e "; |
7 "(Rewrite_Set SqRoot_simplify False) e_e "; |
8 val ttt = (term_of o the o (parseold thy)) |
8 val ttt = (term_of o the o (parseold thy)) |
9 "%e_. (Rewrite_Set SqRoot_simplify False) e_e"; |
9 "%e_. (Rewrite_Set SqRoot_simplify False) e_e"; |
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)"; |
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_::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_])"; |
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)) |
42 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
42 "Script Solve_linear (e_e::bool) (v_v::real)= \ |
43 \(let e_e = \ |
43 \(let e_e = \ |
44 \ (Repeat\ |
44 \ (Repeat\ |
45 \ ((%ee_. (Rewrite_Set_Inst [(bdv,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_])"; |
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_::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_])"; |
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_::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_])"; |
68 atomty ttt; |
68 atomty ttt; |
119 atomt ttt; |
119 atomt ttt; |
120 val ttt = (term_of o the o (parse thy)) |
120 val ttt = (term_of o the o (parse thy)) |
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_::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_])"; |
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_::real)] isolate_bdv False) @@ yyy"; |
131 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy"; |
132 atomty ttt; |
132 atomty ttt; |
133 val ttt = (term_of o the o (parse thy)) |
133 val ttt = (term_of o the o (parse thy)) |
134 "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
134 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\ |
135 \ (Rewrite_Set SqRoot_simplify False)"; |
135 \ (Rewrite_Set SqRoot_simplify False)"; |
136 atomty ttt; |
136 atomty ttt; |
137 val ttt = (term_of o the o (parse thy)) |
137 val ttt = (term_of o the o (parse thy)) |
138 "(Repeat\ |
138 "(Repeat\ |
139 \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
139 \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\ |
140 \ (Rewrite_Set SqRoot_simplify False))) e_e"; |
140 \ (Rewrite_Set SqRoot_simplify False))) e_e"; |
141 atomty ttt; |
141 atomty ttt; |
142 val ttt = (term_of o the o (parseold thy)) |
142 val ttt = (term_of o the o (parseold thy)) |
143 "(let e_e = Repeat xxx e_e in [e_::bool])"; |
143 "(let e_e = Repeat xxx e_e in [e_::bool])"; |
144 atomty ttt; |
144 atomty ttt; |