1 val ttt = (term_of o the o (parse thy)) |
|
2 "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_"; |
|
3 val ttt = (term_of o the o (parse thy)) |
|
4 "(Try (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_)"; |
|
5 |
|
6 val ttt = (term_of o the o (parse thy)) |
|
7 "(Rewrite_Set SqRoot_simplify False) e_ "; |
|
8 val ttt = (term_of o the o (parseold thy)) |
|
9 "%e_. (Rewrite_Set SqRoot_simplify False) e_"; |
|
10 val ttt = (term_of o the o (parseold thy)) |
|
11 "Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_"; |
|
12 |
|
13 val ttt = (term_of o the o (parse thy)) |
|
14 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
15 \[e_]"; |
|
16 val ttt = (term_of o the o (parse thy)) |
|
17 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
18 \((%e_. [e_]) e_)"; |
|
19 val ttt = (term_of o the o (parse thy)) |
|
20 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
21 \((%e_. (let e_ = e_ in [e_])) e_)"; |
|
22 val ttt = (term_of o the o (parse thy)) |
|
23 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
24 \((%e_. \ |
|
25 \ (let e_ = ((Rewrite_Set SqRoot_simplify False) e_)\ |
|
26 \ in [e_]))\ |
|
27 \ e_)"; |
|
28 val ttt = (term_of o the o (parse thy)) |
|
29 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
30 \((%ee_. (let e_ = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_])) e_)"; |
|
31 |
|
32 val ttt = (term_of o the o (parse thy)) |
|
33 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
34 \(let e_ = \ |
|
35 \ (Repeat ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False)) e_)\ |
|
36 \ in [e_])"; |
|
37 (*----*) |
|
38 val ttt = (term_of o the o (parse thy)) |
|
39 |
|
40 (*----*) |
|
41 val ttt = (term_of o the o (parse thy)) |
|
42 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
43 \(let e_ = \ |
|
44 \ (Repeat\ |
|
45 \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\ |
|
46 \ e_)\ |
|
47 \ e_)\ |
|
48 \ in [e_])"; |
|
49 val ttt = (term_of o the o (parse thy)) |
|
50 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
51 \(let e_ = \ |
|
52 \ (Repeat\ |
|
53 \ ((%ee_.\ |
|
54 \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_))\ |
|
55 \ e_)\ |
|
56 \ e_)\ |
|
57 \ in [e_])"; |
|
58 val ttt = (term_of o the o (parse thy)) |
|
59 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
60 \(let e_ = \ |
|
61 \ (Repeat\ |
|
62 \ ((%ee_.\ |
|
63 \ (let e_ = ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\ |
|
64 \ in ((Rewrite_Set SqRoot_simplify False) e_)) )\ |
|
65 \ e_)\ |
|
66 \ e_)\ |
|
67 \ in [e_])"; |
|
68 atomty ttt; |
|
69 atomt ttt; |
|
70 |
|
71 val ttt = (term_of o the o (parse thy)) |
|
72 "Script Testterm (g_::real) = \ |
|
73 \Repeat\ |
|
74 \ (Rewrite rmult_1 False) g_"; |
|
75 val ttt = (term_of o the o (parse thy)) |
|
76 "Script Testterm (g_::real) = \ |
|
77 \Repeat\ |
|
78 \ (((Rewrite rmult_1 False)) Or ((Rewrite rmult_0 False))) g_"; |
|
79 val ttt = (term_of o the o (parse thy)) |
|
80 "Script Testterm (g_::real) = \ |
|
81 \Repeat\ |
|
82 \ ((Repeat (Rewrite rmult_1 False)) Or (Repeat (Rewrite rmult_0 False))) g_"; |
|
83 val ttt = (term_of o the o (parse thy)) |
|
84 "Script Testterm (g_::real) = \ |
|
85 \Repeat\ |
|
86 \ ((Repeat (Rewrite rmult_1 False)) Or\ |
|
87 \ (Repeat (Rewrite rmult_0 False))) g_"; |
|
88 val ttt = (term_of o the o (parse thy)) |
|
89 "Script Testterm (g_::real) = \ |
|
90 \Repeat\ |
|
91 \ ((Repeat (Rewrite rmult_1 False)) Or\ |
|
92 \ (Repeat (Rewrite rmult_0 False)) Or\ |
|
93 \ (Repeat (Rewrite rmult_0 False))) g_"; |
|
94 val ttt = (term_of o the o (parse thy)) |
|
95 "Script Testterm (g_::real) = \ |
|
96 \Repeat\ |
|
97 \ ((Try Repeat (Rewrite rmult_1 False)) Or\ |
|
98 \ (Try Repeat (Rewrite rmult_0 False)) Or\ |
|
99 \ (Try Repeat (Rewrite rmult_0 False))) g_"; |
|
100 |
|
101 |
|
102 |
|
103 |
|
104 |
|
105 |
|
106 |
|
107 |
|
108 |
|
109 |
|
110 |
|
111 |
|
112 |
|
113 (*################### 29.4.02: Rewrite o Rewrite o ...###############*) |
|
114 (*################### 29.4.02: Rewrite o Rewrite o ...###############*) |
|
115 (*################### 29.4.02: Rewrite o Rewrite o ...###############*) |
|
116 |
|
117 |
|
118 |
|
119 atomt ttt; |
|
120 val ttt = (term_of o the o (parse thy)) |
|
121 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
122 \(let e_ = \ |
|
123 \ ((Repeat\ |
|
124 \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
|
125 \ (Rewrite_Set SqRoot_simplify False)))) e_)\ |
|
126 \ in [e_])"; |
|
127 atomty ttt; |
|
128 |
|
129 |
|
130 val ttt = (term_of o the o (parse thy)) |
|
131 "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@ yyy"; |
|
132 atomty ttt; |
|
133 val ttt = (term_of o the o (parse thy)) |
|
134 "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
|
135 \ (Rewrite_Set SqRoot_simplify False)"; |
|
136 atomty ttt; |
|
137 val ttt = (term_of o the o (parse thy)) |
|
138 "(Repeat\ |
|
139 \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
|
140 \ (Rewrite_Set SqRoot_simplify False))) e_"; |
|
141 atomty ttt; |
|
142 val ttt = (term_of o the o (parseold thy)) |
|
143 "(let e_ = Repeat xxx e_ in [e_::bool])"; |
|
144 atomty ttt; |
|
145 val ttt = (term_of o the o (parseold thy)) |
|
146 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
147 \(let e_ = Repeat (xxx) e_ in [e_::bool])"; |
|
148 atomty ttt; |
|
149 val ttt = (term_of o the o (parseold thy)) |
|
150 "Script Solve_linear (e_::bool) (v_::real)= \ |
|
151 \(let e_ =\ |
|
152 \ Repeat\ |
|
153 \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ |
|
154 \ (Rewrite_Set SqRoot_simplify False))) e_\ |
|
155 \ in [e_::bool])" |
|
156 ; |
|
157 atomty ttt; |
|
158 |
|