1.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 16:45:27 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 16:47:22 2010 +0200
1.3 @@ -597,7 +597,7 @@
1.4 "Script Solve_linear (e_e::bool) (v_v::real)= " ^
1.5 "(let e_e =" ^
1.6 " Repeat" ^
1.7 - " (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^
1.8 + " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
1.9 " (Rewrite_Set Test_simplify False))) e_e" ^
1.10 " in [e_::bool])"
1.11 )
1.12 @@ -897,7 +897,7 @@
1.13 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1.14 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.15 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1.16 - " (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^
1.17 + " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
1.18 " (Try (Rewrite_Set Test_simplify False)))" ^
1.19 " e_e" ^
1.20 " in [e_::bool])"
1.21 @@ -927,12 +927,12 @@
1.22 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1.23 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.24 " (Try (Rewrite_Set Test_simplify False)) @@" ^
1.25 - " (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^
1.26 + " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
1.27 " (Try (Rewrite_Set Test_simplify False)))" ^
1.28 - " e_;" ^
1.29 + " e_e;" ^
1.30 " (L_::bool list) = Tac subproblem_equation_dummy; " ^
1.31 - " L_ = Tac solve_equation_dummy " ^
1.32 - " in Check_elementwise L_ {(v_v::real). Assumptions})"
1.33 + " L_L = Tac solve_equation_dummy " ^
1.34 + " in Check_elementwise L_L {(v_v::real). Assumptions})"
1.35 ));
1.36
1.37 store_met
1.38 @@ -946,10 +946,10 @@
1.39 crls=tval_rls, nrls=Test_simplify},
1.40 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.41 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.42 - " (Try (Rewrite_Set Test_simplify False))) e_; " ^
1.43 + " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
1.44 "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.45 " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
1.46 - "in Check_elementwise L_ {(v_v::real). Assumptions})"
1.47 + "in Check_elementwise L_L {(v_v::real). Assumptions})"
1.48 ));
1.49
1.50 store_met
1.51 @@ -964,10 +964,10 @@
1.52 asm_rls=[],asm_thm=[("square_equation_left",""),
1.53 ("square_equation_right","")]*)},
1.54 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.55 - " (let e_e = Try (Rewrite_Set norm_equation False) e_; " ^
1.56 + " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
1.57 "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.58 " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_])" ^
1.59 - "in Check_elementwise L_ {(v_v::real). Assumptions})"
1.60 + "in Check_elementwise L_L {(v_v::real). Assumptions})"
1.61 ));
1.62
1.63 store_met
1.64 @@ -994,11 +994,11 @@
1.65 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1.66 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.67 " (Try (Rewrite_Set Test_simplify False)))" ^
1.68 - " e_;" ^
1.69 + " e_e;" ^
1.70 " (L_::bool list) = " ^
1.71 " (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.72 " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
1.73 - "in Check_elementwise L_ {(v_v::real). Assumptions})"
1.74 + "in Check_elementwise L_L {(v_v::real). Assumptions})"
1.75 ));
1.76
1.77 store_met
1.78 @@ -1025,10 +1025,10 @@
1.79 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1.80 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.81 " (Try (Rewrite_Set Test_simplify False)))" ^
1.82 - " e_;" ^
1.83 + " e_e;" ^
1.84 " (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.85 " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
1.86 - " in Check_elementwise L_ {(v_v::real). Assumptions})"
1.87 + " in Check_elementwise L_L {(v_v::real). Assumptions})"
1.88 ));
1.89
1.90 store_met
1.91 @@ -1056,10 +1056,10 @@
1.92 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1.93 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.94 " (Try (Rewrite_Set Test_simplify False)))" ^
1.95 - " e_;" ^
1.96 + " e_e;" ^
1.97 " (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^
1.98 " [Test,solve_plain_square]) [BOOL e_e, REAL v_])" ^
1.99 - " in Check_elementwise L_ {(v_v::real). Assumptions})"
1.100 + " in Check_elementwise L_L {(v_v::real). Assumptions})"
1.101 ));
1.102
1.103 store_met
1.104 @@ -1087,10 +1087,10 @@
1.105 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
1.106 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.107 " (Try (Rewrite_Set Test_simplify False)))" ^
1.108 - " e_;" ^
1.109 + " e_e;" ^
1.110 " (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^
1.111 " [no_met]) [BOOL e_e, REAL v_])" ^
1.112 - " in Check_elementwise L_ {(v_v::real). Assumptions})"
1.113 + " in Check_elementwise L_L {(v_v::real). Assumptions})"
1.114 ) ); (*#######*)
1.115
1.116 store_met
1.117 @@ -1200,9 +1200,9 @@
1.118 end
1.119 | ord => ord)
1.120 and hd_ord (f, g) = (* ~ term.ML *)
1.121 - prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.122 + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.123 and terms_ord str pr (ts, us) =
1.124 - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
1.125 + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
1.126 in
1.127
1.128 fun ord_make_polytest (pr:bool) thy (_:subst) tu =