1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  consts
     1.6  
     1.7 -  occur'_exactly'_in :: 
     1.8 +  occur_exactly_in :: 
     1.9     "[real list, real list, 'a] => bool" ("_ from _ occur'_exactly'_in _")
    1.10  
    1.11    (*descriptions in the related problems*)
    1.12 @@ -66,10 +66,10 @@
    1.13                                            (subtract op = vs all)))
    1.14      end;
    1.15  
    1.16 -(*("occur_exactly_in", ("EqSystem.occur'_exactly'_in", 
    1.17 +(*("occur_exactly_in", ("EqSystem.occur_exactly_in", 
    1.18  			eval_occur_exactly_in "#eval_occur_exactly_in_"))*)
    1.19 -fun eval_occur_exactly_in _ "EqSystem.occur'_exactly'_in"
    1.20 -			  (p as (Const ("EqSystem.occur'_exactly'_in",_) 
    1.21 +fun eval_occur_exactly_in _ "EqSystem.occur_exactly_in"
    1.22 +			  (p as (Const ("EqSystem.occur_exactly_in",_) 
    1.23  				       $ vs $ all $ t)) _ =
    1.24      if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
    1.25      then SOME ((UnparseC.term p) ^ " = True",
    1.26 @@ -80,7 +80,7 @@
    1.27  \<close>
    1.28  setup \<open>KEStore_Elems.add_calcs
    1.29    [("occur_exactly_in",
    1.30 -	    ("EqSystem.occur'_exactly'_in",
    1.31 +	    ("EqSystem.occur_exactly_in",
    1.32  	      eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close>
    1.33  ML \<open>
    1.34  (** rewrite order 'ord_simplify_System' **)
    1.35 @@ -292,7 +292,7 @@
    1.36      Rule_Def.Repeat {id="isolate_bdvs", preconds = [], 
    1.37  	 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.38  	 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty 
    1.39 -			   [(Rule.Eval ("EqSystem.occur'_exactly'_in", 
    1.40 +			   [(Rule.Eval ("EqSystem.occur_exactly_in", 
    1.41  				   eval_occur_exactly_in 
    1.42  				       "#eval_occur_exactly_in_"))
    1.43  			    ], 
    1.44 @@ -309,10 +309,10 @@
    1.45  	 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), 
    1.46  	 erls = Rule_Set.append_rules 
    1.47  		    "erls_isolate_bdvs_4x4" Rule_Set.empty 
    1.48 -		    [Rule.Eval ("EqSystem.occur'_exactly'_in", 
    1.49 +		    [Rule.Eval ("EqSystem.occur_exactly_in", 
    1.50  			   eval_occur_exactly_in "#eval_occur_exactly_in_"),
    1.51  		     Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
    1.52 -		     Rule.Eval ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
    1.53 +		     Rule.Eval ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
    1.54           Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
    1.55  		     Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
    1.56  			    ], 
    1.57 @@ -357,7 +357,7 @@
    1.58  		  Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
    1.59  		  Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
    1.60  		  Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
    1.61 -		  Rule.Eval ("EqSystem.occur'_exactly'_in", 
    1.62 +		  Rule.Eval ("EqSystem.occur_exactly_in", 
    1.63  			eval_occur_exactly_in 
    1.64  			    "#eval_occur_exactly_in_")
    1.65  		  ],
    1.66 @@ -386,7 +386,7 @@
    1.67  		  Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
    1.68  		  Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
    1.69  		  Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
    1.70 -		  Rule.Eval ("EqSystem.occur'_exactly'_in", 
    1.71 +		  Rule.Eval ("EqSystem.occur_exactly_in", 
    1.72  			eval_occur_exactly_in 
    1.73  			    "#eval_occur_exactly_in_")
    1.74  		  ],
    1.75 @@ -481,7 +481,7 @@
    1.76                "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
    1.77            ("#Find"  ,["solution ss'''"])],
    1.78        Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
    1.79 -	      [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], 
    1.80 +	      [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")], 
    1.81        SOME "solveSystem e_s v_s", 
    1.82        [["EqSystem", "top_down_substitution", "4x4"]])),
    1.83      (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
    1.84 @@ -660,10 +660,12 @@
    1.85  	    {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [], 
    1.86  	      srls = Rule_Set.append_rules "srls_top_down_4x4" srls [], 
    1.87  	      prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
    1.88 -			      [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], 
    1.89 +			      [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")], 
    1.90  	      crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
    1.91  	    (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
    1.92  	    @{thm solve_system4.simps})]
    1.93 +\<close> ML \<open>
    1.94 +\<close> ML \<open>
    1.95 +\<close> ML \<open>
    1.96  \<close>
    1.97 -
    1.98 -end
    1.99 \ No newline at end of file
   1.100 +end