
diff -r 8cba439d0454 -r 68883c046963 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Tue Apr 21 12:26:08 2020 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Tue Apr 21 15:42:50 2020 +0200
@@ -406,18 +406,18 @@
 
 (** problems **)
 setup \<open>KEStore_Elems.add_pbts
-  [(Specify.prep_pbt thy "pbl_equsys" [] Celem.e_pblID
+  [(Specify.prep_pbt thy "pbl_equsys" [] Spec.e_pblID
       (["system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Find"  ,["solution ss'''"](*''' is copy-named*))],
         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
-    (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID
+    (Specify.prep_pbt thy "pbl_equsys_lin" [] Spec.e_pblID
       (["LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           (*TODO.WN050929 check linearity*)
           ("#Find"  ,["solution ss'''"])],
         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
-    (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID
+    (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Spec.e_pblID
       (["2x2", "LINEAR", "system"],
       (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
@@ -429,7 +429,7 @@
 			      Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
 			      Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")], 
         SOME "solveSystem e_s v_s", [])),
-    (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Celem.e_pblID
+    (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Spec.e_pblID
       (["triangular", "2x2", "LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Where",
@@ -437,14 +437,14 @@
               "    v_s  from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
           ("#Find"  ,["solution ss'''"])],
         prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])),
-    (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Celem.e_pblID
+    (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Spec.e_pblID
       (["normalise", "2x2", "LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Find"  ,["solution ss'''"])],
       Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
       SOME "solveSystem e_s v_s", 
       [["EqSystem","normalise","2x2"]])),
-    (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID
+    (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Spec.e_pblID
       (["3x3", "LINEAR", "system"],
         (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
@@ -456,7 +456,7 @@
 			      Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
 			      Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
         SOME "solveSystem e_s v_s", [])),
-    (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Celem.e_pblID
+    (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Spec.e_pblID
       (["4x4", "LINEAR", "system"],
         (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
@@ -468,7 +468,7 @@
 			      Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
 			      Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
         SOME "solveSystem e_s v_s", [])),
-    (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Celem.e_pblID
+    (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Spec.e_pblID
       (["triangular", "4x4", "LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Where" , (*accepts missing variables up to diagional form*)
@@ -481,7 +481,7 @@
 	      [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], 
       SOME "solveSystem e_s v_s", 
       [["EqSystem","top_down_substitution","4x4"]])),
-    (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Celem.e_pblID
+    (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Spec.e_pblID
       (["normalise", "4x4", "LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           (*LENGTH is checked 1 level above*)
@@ -510,12 +510,12 @@
 
 (**methods**)
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
+    [Specify.prep_met thy "met_eqsys" [] Spec.e_metID
 	    (["EqSystem"], [],
 	      {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
           errpats = [], nrls = Rule_Set.Empty},
 	      @{thm refl}),
-    Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
+    Specify.prep_met thy "met_eqsys_topdown" [] Spec.e_metID
       (["EqSystem","top_down_substitution"], [],
         {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
           errpats = [], nrls = Rule_Set.Empty},
@@ -542,7 +542,7 @@
   in
     Try (Rewrite_Set ''order_system'' ) e__s)                              "
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
+    [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Spec.e_metID
       (["EqSystem", "top_down_substitution", "2x2"],
         [("#Given", ["equalities e_s", "solveForVars v_s"]),
           ("#Where",
@@ -558,7 +558,7 @@
 	      @{thm solve_system.simps})]
 \<close>
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
+    [Specify.prep_met thy "met_eqsys_norm" [] Spec.e_metID
 	    (["EqSystem", "normalise"], [],
 	      {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
           errpats = [], nrls = Rule_Set.Empty},
@@ -580,7 +580,7 @@
     SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
       [BOOL_LIST e__s, REAL_LIST v_s])"
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
+    [Specify.prep_met thy "met_eqsys_norm_2x2" [] Spec.e_metID
 	    (["EqSystem","normalise","2x2"],
 	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 		      ("#Find"  ,["solution ss'''"])],
@@ -612,7 +612,7 @@
     SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
       [BOOL_LIST e__s, REAL_LIST v_s])"
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
+    [Specify.prep_met thy "met_eqsys_norm_4x4" [] Spec.e_metID
 	      (["EqSystem","normalise","4x4"],
 	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	         ("#Find"  ,["solution ss'''"])],
@@ -644,7 +644,7 @@
   in
     [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
+    [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Spec.e_metID
 	    (["EqSystem","top_down_substitution","4x4"],
 	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	        ("#Where" , (*accepts missing variables up to diagonal form*)




