
diff -r d1b52fcd4023 -r 229e5c9cf78b src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Sun Mar 25 13:59:57 2018 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Mar 26 07:28:39 2018 +0200
@@ -32,41 +32,41 @@
 val thy = @{theory};
 
 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
-  Celem.append_rls "LinEq_prls" Celem.e_rls 
-	     [Celem.Calc ("HOL.eq",eval_equal "#equal_"),
-	      Celem.Calc ("Tools.matches",eval_matches ""),
-	      Celem.Calc ("Tools.lhs"    ,eval_lhs ""),
-	      Celem.Calc ("Tools.rhs"    ,eval_rhs ""),
-	      Celem.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
- 	      Celem.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
-	      Celem.Calc ("Atools.occurs'_in",eval_occurs_in ""),    
-	      Celem.Calc ("Atools.ident",eval_ident "#ident_"),
-	      Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
-	      Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
-	      Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
-	      Celem.Thm ("and_false",TermC.num_str @{thm and_false}),
-	      Celem.Thm ("or_true",TermC.num_str @{thm or_true}),
-	      Celem.Thm ("or_false",TermC.num_str @{thm or_false})
+  Rule.append_rls "LinEq_prls" Rule.e_rls 
+	     [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
+	      Rule.Calc ("Tools.matches",eval_matches ""),
+	      Rule.Calc ("Tools.lhs"    ,eval_lhs ""),
+	      Rule.Calc ("Tools.rhs"    ,eval_rhs ""),
+	      Rule.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
+ 	      Rule.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
+	      Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),    
+	      Rule.Calc ("Atools.ident",eval_ident "#ident_"),
+	      Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
+	      Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
+	      Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
+	      Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
+	      Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
+	      Rule.Thm ("or_false",TermC.num_str @{thm or_false})
               ];
 (* ----- erls ----- *)
 val LinEq_crls = 
-   Celem.append_rls "LinEq_crls" poly_crls
-   [Celem.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
+   Rule.append_rls "LinEq_crls" poly_crls
+   [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
     (*		
      Don't use
-     Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
-     Celem.Calc ("Atools.pow" ,eval_binop "#power_"),
+     Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
+     Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
      *)
     ];
 
 (* ----- crls ----- *)
 val LinEq_erls = 
-   Celem.append_rls "LinEq_erls" Poly_erls
-   [Celem.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
+   Rule.append_rls "LinEq_erls" Poly_erls
+   [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
     (*		
      Don't use
-     Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
-     Celem.Calc ("Atools.pow" ,eval_binop "#power_"),
+     Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
+     Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
      *)
     ];
 *}
@@ -75,23 +75,23 @@
 ML {*
     
 val LinPoly_simplify = prep_rls'(
-  Celem.Rls {id = "LinPoly_simplify", preconds = [], 
+  Rule.Rls {id = "LinPoly_simplify", preconds = [], 
        rew_ord = ("termlessI",termlessI), 
        erls = LinEq_erls, 
-       srls = Celem.Erls, 
+       srls = Rule.Erls, 
        calc = [], errpatts = [],
        rules = [
-		Celem.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
-		Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
-		Celem.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
-		Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"),
+		Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
+		Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
+		Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
+		Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
 		(*  Dont use  
-		 Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),		
-		 Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
+		 Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),		
+		 Rule.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
 		 *)
-		Celem.Calc ("Atools.pow" ,eval_binop "#power_")
+		Rule.Calc ("Atools.pow" ,eval_binop "#power_")
 		],
-       scr = Celem.EmptyScr});
+       scr = Rule.EmptyScr});
 *}
 setup {* KEStore_Elems.add_rlss 
   [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *}
@@ -99,20 +99,20 @@
 
 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
 val LinEq_simplify = prep_rls'(
-Celem.Rls {id = "LinEq_simplify", preconds = [],
-     rew_ord = ("e_rew_ord", Celem.e_rew_ord),
+Rule.Rls {id = "LinEq_simplify", preconds = [],
+     rew_ord = ("e_rew_ord", Rule.e_rew_ord),
      erls = LinEq_erls,
-     srls = Celem.Erls,
+     srls = Rule.Erls,
      calc = [], errpatts = [],
      rules = [
-	      Celem.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}), 
+	      Rule.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}), 
 	      (* a+bx=0 -> bx=-a *)
-	      Celem.Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}), 
+	      Rule.Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}), 
 	      (* a+ x=0 ->  x=-a *)
-	      Celem.Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div})    
+	      Rule.Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div})    
 	      (*   bx=c -> x=c/b *)  
 	      ],
-     scr = Celem.EmptyScr});
+     scr = Rule.EmptyScr});
 *}
 setup {* KEStore_Elems.add_rlss 
   [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *}
@@ -135,7 +135,7 @@
 setup {* KEStore_Elems.add_mets
   [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
       (["LinEq"], [],
-        {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
+        {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
           crls = LinEq_crls, errpats = [], nrls = norm_Poly},
         "empty_script"),
     (* ansprechen mit ["LinEq","solve_univar_equation"] *)
@@ -144,7 +144,7 @@
         [("#Given", ["equality e_e", "solveFor v_v"]),
           ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),
           ("#Find",  ["solutions v_v'i'"])],
-        {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Celem.e_rls, prls = LinEq_prls, calc = [],
+        {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],
           crls = LinEq_crls, errpats = [], nrls = norm_Poly},
         "Script Solve_lineq_equation (e_e::bool) (v_v::real) =                 " ^
           "(let e_e =((Try         (Rewrite      all_left           False)) @@   " ^ 




