1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  consts
     1.5  
     1.6    Integral            :: "[real, real]=> real" ("Integral _ D _" 91)
     1.7 -(*new'_c	      :: "real => real"        ("new'_c _" 66)*)
     1.8 -  is'_f'_x            :: "real => bool"        ("_ is'_f'_x" 10)
     1.9 +(*new_c	      :: "real => real"        ("new_c _" 66)*)
    1.10 +  is_f_x            :: "real => bool"        ("_ is'_f'_x" 10)
    1.11  
    1.12    (*descriptions in the related problems*)
    1.13    integrateBy         :: "real => una"
    1.14 @@ -72,18 +72,18 @@
    1.15      end;
    1.16  
    1.17  (*WN080222
    1.18 -(*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
    1.19 -fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
    1.20 +(*("new_c", ("Integrate.new_c", eval_new_c "#new_c_"))*)
    1.21 +fun eval_new_c _ _ (p as (Const ("Integrate.new_c",_) $ t)) _ =
    1.22       SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (new_c p),
    1.23  	  Trueprop $ (mk_equality (p, new_c p)))
    1.24    | eval_new_c _ _ _ _ = NONE;
    1.25  *)
    1.26  
    1.27  (*WN080222:*)
    1.28 -(*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_"))
    1.29 +(*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
    1.30    add a new c to a term or a fun-equation;
    1.31    this is _not in_ the term, because only applied to _whole_ term*)
    1.32 -fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
    1.33 +fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:theory) =
    1.34      let val p' = case p of
    1.35  		     Const ("HOL.eq", T) $ lh $ rh => 
    1.36  		     Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
    1.37 @@ -94,8 +94,8 @@
    1.38    | eval_add_new_c _ _ _ _ = NONE;
    1.39  
    1.40  
    1.41 -(*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
    1.42 -fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
    1.43 +(*("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_x_"))*)
    1.44 +fun eval_is_f_x _ _(p as (Const ("Integrate.is_f_x", _)
    1.45  					   $ arg)) _ =
    1.46      if TermC.is_f_x arg
    1.47      then SOME ((UnparseC.term p) ^ " = True",
    1.48 @@ -105,8 +105,8 @@
    1.49    | eval_is_f_x _ _ _ _ = NONE;
    1.50  \<close>
    1.51  setup \<open>KEStore_Elems.add_calcs
    1.52 -  [("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
    1.53 -    ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))]\<close>
    1.54 +  [("add_new_c", ("Integrate.add_new_c", eval_add_new_c "add_new_c_")),
    1.55 +    ("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_idextifier_"))]\<close>
    1.56  ML \<open>
    1.57  (** rulesets **)
    1.58  
    1.59 @@ -120,7 +120,7 @@
    1.60  		     erls = Rule_Set.Empty, 
    1.61  		     srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.62  		     rules = [(*for rewriting conditions in Thm's*)
    1.63 -			      Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
    1.64 +			      Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
    1.65  			      Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
    1.66  			      Rule.Thm ("not_false",@{thm not_false})
    1.67  			      ],
    1.68 @@ -146,7 +146,7 @@
    1.69  		     erls = Rule_Set.Empty, 
    1.70  		     srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.71  		     rules = [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches""),
    1.72 -			      Rule.Eval ("Integrate.is'_f'_x", 
    1.73 +			      Rule.Eval ("Integrate.is_f_x", 
    1.74  				    eval_is_f_x "is_f_x_"),
    1.75  			      Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
    1.76  			      Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
    1.77 @@ -154,7 +154,7 @@
    1.78  		     scr = Rule.Empty_Prog}, 
    1.79  	 srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.80  	 rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*)
    1.81 -		   Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
    1.82 +		   Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")
    1.83  		   ],
    1.84  	 scr = Rule.Empty_Prog};
    1.85  \<close>
    1.86 @@ -173,7 +173,7 @@
    1.87  		       rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.88  		       erls = (*FIXME.WN051028 Rule_Set.empty,*)
    1.89  		       Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
    1.90 -				  [Rule.Eval ("Poly.is'_polyexp", 
    1.91 +				  [Rule.Eval ("Poly.is_polyexp", 
    1.92  					 eval_is_polyexp "")],
    1.93  				  srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.94  				  rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
    1.95 @@ -384,6 +384,8 @@
    1.96  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.97            crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
    1.98          @{thm intergrate_named.simps})]
    1.99 +\<close> ML \<open>
   1.100 +\<close> ML \<open>
   1.101  \<close>
   1.102  
   1.103  end
   1.104 \ No newline at end of file