1.1 --- a/src/Tools/isac/IsacKnowledge/Test.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,158 +0,0 @@
1.4 -val ttt = (term_of o the o (parse thy))
1.5 -"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_";
1.6 -val ttt = (term_of o the o (parse thy))
1.7 -"(Try (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_)";
1.8 -
1.9 -val ttt = (term_of o the o (parse thy))
1.10 - "(Rewrite_Set SqRoot_simplify False) e_ ";
1.11 -val ttt = (term_of o the o (parseold thy))
1.12 - "%e_. (Rewrite_Set SqRoot_simplify False) e_";
1.13 -val ttt = (term_of o the o (parseold thy))
1.14 - "Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_";
1.15 -
1.16 -val ttt = (term_of o the o (parse thy))
1.17 - "Script Solve_linear (e_::bool) (v_::real)= \
1.18 - \[e_]";
1.19 -val ttt = (term_of o the o (parse thy))
1.20 - "Script Solve_linear (e_::bool) (v_::real)= \
1.21 - \((%e_. [e_]) e_)";
1.22 -val ttt = (term_of o the o (parse thy))
1.23 - "Script Solve_linear (e_::bool) (v_::real)= \
1.24 - \((%e_. (let e_ = e_ in [e_])) e_)";
1.25 -val ttt = (term_of o the o (parse thy))
1.26 - "Script Solve_linear (e_::bool) (v_::real)= \
1.27 - \((%e_. \
1.28 - \ (let e_ = ((Rewrite_Set SqRoot_simplify False) e_)\
1.29 - \ in [e_]))\
1.30 - \ e_)";
1.31 -val ttt = (term_of o the o (parse thy))
1.32 - "Script Solve_linear (e_::bool) (v_::real)= \
1.33 - \((%ee_. (let e_ = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_])) e_)";
1.34 -
1.35 -val ttt = (term_of o the o (parse thy))
1.36 - "Script Solve_linear (e_::bool) (v_::real)= \
1.37 - \(let e_ = \
1.38 - \ (Repeat ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False)) e_)\
1.39 - \ in [e_])";
1.40 -(*----*)
1.41 -val ttt = (term_of o the o (parse thy))
1.42 -
1.43 -(*----*)
1.44 -val ttt = (term_of o the o (parse thy))
1.45 - "Script Solve_linear (e_::bool) (v_::real)= \
1.46 - \(let e_ = \
1.47 - \ (Repeat\
1.48 - \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\
1.49 - \ e_)\
1.50 - \ e_)\
1.51 - \ in [e_])";
1.52 -val ttt = (term_of o the o (parse thy))
1.53 - "Script Solve_linear (e_::bool) (v_::real)= \
1.54 - \(let e_ = \
1.55 - \ (Repeat\
1.56 - \ ((%ee_.\
1.57 - \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_))\
1.58 - \ e_)\
1.59 - \ e_)\
1.60 - \ in [e_])";
1.61 -val ttt = (term_of o the o (parse thy))
1.62 - "Script Solve_linear (e_::bool) (v_::real)= \
1.63 - \(let e_ = \
1.64 - \ (Repeat\
1.65 - \ ((%ee_.\
1.66 - \ (let e_ = ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\
1.67 - \ in ((Rewrite_Set SqRoot_simplify False) e_)) )\
1.68 - \ e_)\
1.69 - \ e_)\
1.70 - \ in [e_])";
1.71 -atomty ttt;
1.72 -atomt ttt;
1.73 -
1.74 -val ttt = (term_of o the o (parse thy))
1.75 - "Script Testterm (g_::real) = \
1.76 - \Repeat\
1.77 - \ (Rewrite rmult_1 False) g_";
1.78 -val ttt = (term_of o the o (parse thy))
1.79 - "Script Testterm (g_::real) = \
1.80 - \Repeat\
1.81 - \ (((Rewrite rmult_1 False)) Or ((Rewrite rmult_0 False))) g_";
1.82 -val ttt = (term_of o the o (parse thy))
1.83 - "Script Testterm (g_::real) = \
1.84 - \Repeat\
1.85 - \ ((Repeat (Rewrite rmult_1 False)) Or (Repeat (Rewrite rmult_0 False))) g_";
1.86 -val ttt = (term_of o the o (parse thy))
1.87 - "Script Testterm (g_::real) = \
1.88 - \Repeat\
1.89 - \ ((Repeat (Rewrite rmult_1 False)) Or\
1.90 - \ (Repeat (Rewrite rmult_0 False))) g_";
1.91 -val ttt = (term_of o the o (parse thy))
1.92 - "Script Testterm (g_::real) = \
1.93 - \Repeat\
1.94 - \ ((Repeat (Rewrite rmult_1 False)) Or\
1.95 - \ (Repeat (Rewrite rmult_0 False)) Or\
1.96 - \ (Repeat (Rewrite rmult_0 False))) g_";
1.97 -val ttt = (term_of o the o (parse thy))
1.98 - "Script Testterm (g_::real) = \
1.99 - \Repeat\
1.100 - \ ((Try Repeat (Rewrite rmult_1 False)) Or\
1.101 - \ (Try Repeat (Rewrite rmult_0 False)) Or\
1.102 - \ (Try Repeat (Rewrite rmult_0 False))) g_";
1.103 -
1.104 -
1.105 -
1.106 -
1.107 -
1.108 -
1.109 -
1.110 -
1.111 -
1.112 -
1.113 -
1.114 -
1.115 -
1.116 -(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
1.117 -(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
1.118 -(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
1.119 -
1.120 -
1.121 -
1.122 -atomt ttt;
1.123 -val ttt = (term_of o the o (parse thy))
1.124 - "Script Solve_linear (e_::bool) (v_::real)= \
1.125 - \(let e_ = \
1.126 - \ ((Repeat\
1.127 - \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.128 - \ (Rewrite_Set SqRoot_simplify False)))) e_)\
1.129 - \ in [e_])";
1.130 -atomty ttt;
1.131 -
1.132 -
1.133 -val ttt = (term_of o the o (parse thy))
1.134 -"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@ yyy";
1.135 -atomty ttt;
1.136 -val ttt = (term_of o the o (parse thy))
1.137 - "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.138 - \ (Rewrite_Set SqRoot_simplify False)";
1.139 -atomty ttt;
1.140 -val ttt = (term_of o the o (parse thy))
1.141 - "(Repeat\
1.142 - \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.143 - \ (Rewrite_Set SqRoot_simplify False))) e_";
1.144 -atomty ttt;
1.145 -val ttt = (term_of o the o (parseold thy))
1.146 -"(let e_ = Repeat xxx e_ in [e_::bool])";
1.147 -atomty ttt;
1.148 -val ttt = (term_of o the o (parseold thy))
1.149 - "Script Solve_linear (e_::bool) (v_::real)= \
1.150 - \(let e_ = Repeat (xxx) e_ in [e_::bool])";
1.151 -atomty ttt;
1.152 -val ttt = (term_of o the o (parseold thy))
1.153 - "Script Solve_linear (e_::bool) (v_::real)= \
1.154 - \(let e_ =\
1.155 - \ Repeat\
1.156 - \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
1.157 - \ (Rewrite_Set SqRoot_simplify False))) e_\
1.158 - \ in [e_::bool])"
1.159 -;
1.160 -atomty ttt;
1.161 -