1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy	Thu Jun 10 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy	Thu Jun 10 12:48:50 2021 +0200
     1.3 @@ -19,9 +19,6 @@
     1.4    senkrecht       :: real
     1.5    unten           :: real
     1.6  
     1.7 -ML \<open>
     1.8 -val thy = @{theory};
     1.9 -\<close>
    1.10  (** problems **)
    1.11  setup \<open>KEStore_Elems.add_pbts
    1.12    [(Problem.prep_input @{theory} "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])),

     2.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Thu Jun 10 12:23:57 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Thu Jun 10 12:48:50 2021 +0200
     2.3 @@ -87,8 +87,6 @@
     2.4    realpow_pow_bdv: "(bdv \<up> b) \<up> c = bdv \<up> (b * c)"
     2.5  
     2.6  ML \<open>
     2.7 -val thy = @{theory};
     2.8 -
     2.9  (** eval functions **)
    2.10  
    2.11  fun primed (Const (id, T)) = Const (id ^ "'", T)
    2.12 @@ -266,10 +264,10 @@
    2.13     val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
    2.14     *)
    2.15  fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
    2.16 -    [((Thm.term_of o the o (TermC.parse thy)) "functionTerm", [t]),
    2.17 -     ((Thm.term_of o the o (TermC.parse thy)) "differentiateFor", [bdv]),
    2.18 -     ((Thm.term_of o the o (TermC.parse thy)) "derivative", 
    2.19 -      [(Thm.term_of o the o (TermC.parse thy)) "f_f'"])
    2.20 +    [((Thm.term_of o the o (TermC.parse \<^theory>)) "functionTerm", [t]),
    2.21 +     ((Thm.term_of o the o (TermC.parse \<^theory>)) "differentiateFor", [bdv]),
    2.22 +     ((Thm.term_of o the o (TermC.parse \<^theory>)) "derivative", 
    2.23 +      [(Thm.term_of o the o (TermC.parse \<^theory>)) "f_f'"])
    2.24       ]
    2.25    | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
    2.26  \<close>
    2.27 @@ -423,10 +421,10 @@
    2.28     val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
    2.29     *)
    2.30  fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
    2.31 -    [((Thm.term_of o the o (TermC.parse thy)) "functionEq", [t]),
    2.32 -     ((Thm.term_of o the o (TermC.parse thy)) "differentiateFor", [bdv]),
    2.33 -     ((Thm.term_of o the o (TermC.parse thy)) "derivativeEq", 
    2.34 -      [(Thm.term_of o the o (TermC.parse thy)) "f_f'::bool"])
    2.35 +    [((Thm.term_of o the o (TermC.parse \<^theory>)) "functionEq", [t]),
    2.36 +     ((Thm.term_of o the o (TermC.parse \<^theory>)) "differentiateFor", [bdv]),
    2.37 +     ((Thm.term_of o the o (TermC.parse \<^theory>)) "derivativeEq", 
    2.38 +      [(Thm.term_of o the o (TermC.parse \<^theory>)) "f_f'::bool"])
    2.39       ]
    2.40    | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
    2.41  \<close>

     3.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Thu Jun 10 12:23:57 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Thu Jun 10 12:48:50 2021 +0200
     3.3 @@ -32,8 +32,6 @@
     3.4  \<close>
     3.5  
     3.6  ML \<open>
     3.7 -val thy = @{theory};
     3.8 -
     3.9  val eval_rls = prep_rls' (
    3.10    Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI), 
    3.11      erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],

     4.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Jun 10 12:23:57 2021 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Jun 10 12:48:50 2021 +0200
     4.3 @@ -11,8 +11,6 @@
     4.4  axiomatization where
     4.5    int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
     4.6  
     4.7 -ML \<open>val thy = @{theory}\<close>
     4.8 -
     4.9  text \<open>problemclass for the usecase\<close>
    4.10  setup \<open>KEStore_Elems.add_pbts
    4.11    [(Problem.prep_input @{theory} "pbl_equ_dio" [] Problem.id_empty

     5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Thu Jun 10 12:23:57 2021 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Jun 10 12:48:50 2021 +0200
     5.3 @@ -49,8 +49,6 @@
     5.4      works for lists of any length, interestingly !?!*)
     5.5  
     5.6  ML \<open>
     5.7 -val thy = @{theory};
     5.8 -
     5.9  (** eval functions **)
    5.10  
    5.11  (*certain variables of a given list occur _all_ in a term
    5.12 @@ -163,7 +161,7 @@
    5.13  end;
    5.14  (**)
    5.15  Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
    5.16 -[("ord_simplify_System", ord_simplify_System false thy)
    5.17 +[("ord_simplify_System", ord_simplify_System false \<^theory>)
    5.18   ]);
    5.19  \<close>
    5.20  ML \<open>
    5.21 @@ -332,7 +330,7 @@
    5.22  val order_system = 
    5.23      Rule_Def.Repeat {id="order_system", preconds = [], 
    5.24  	 rew_ord = ("ord_simplify_System", 
    5.25 -		    ord_simplify_System false thy), 
    5.26 +		    ord_simplify_System false \<^theory>), 
    5.27  	 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    5.28  	 rules = [Rule.Thm ("order_system_NxN", ThmC.numerals_to_Free @{thm order_system_NxN})
    5.29  		  ],

     6.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Thu Jun 10 12:23:57 2021 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Thu Jun 10 12:48:50 2021 +0200
     6.3 @@ -33,9 +33,6 @@
     6.4          (c) by Richard Lang, 2003\<close>
     6.5  
     6.6  ML \<open>
     6.7 -val thy = @{theory};
     6.8 -val ctxt = ThyC.to_ctxt thy;
     6.9 -
    6.10  val univariate_equation_prls = 
    6.11      Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty 
    6.12  	       [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
    6.13 @@ -65,10 +62,10 @@
    6.14  				  "solveTest (x+1=2, x)");
    6.15     *)
    6.16  fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
    6.17 -    [((the o (TermC.parseNEW ctxt)) "equality", [eq]),
    6.18 -     ((the o (TermC.parseNEW ctxt)) "solveFor", [bdv]),
    6.19 -     ((the o (TermC.parseNEW ctxt)) "solutions", 
    6.20 -      [(the o (TermC.parseNEW ctxt)) "L"])
    6.21 +    [((the o (TermC.parseNEW \<^context>)) "equality", [eq]),
    6.22 +     ((the o (TermC.parseNEW \<^context>)) "solveFor", [bdv]),
    6.23 +     ((the o (TermC.parseNEW \<^context>)) "solutions", 
    6.24 +      [(the o (TermC.parseNEW \<^context>)) "L"])
    6.25       ]
    6.26    | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss";
    6.27  \<close>

     7.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Jun 10 12:23:57 2021 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Jun 10 12:48:50 2021 +0200
     7.3 @@ -41,8 +41,6 @@
     7.4  (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
     7.5  
     7.6  ML \<open>
     7.7 -val thy = @{theory};
     7.8 -
     7.9  (** eval functions **)
    7.10  
    7.11  val c = Free ("c", HOLogic.realT);

     8.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Jun 10 12:23:57 2021 +0200
     8.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Jun 10 12:48:50 2021 +0200
     8.3 @@ -42,9 +42,7 @@
     8.4  rule_set_knowledge inverse_z = inverse_z
     8.5  
     8.6  subsection\<open>Define the Specification\<close>
     8.7 -ML \<open>
     8.8 -val thy = @{theory};
     8.9 -\<close>
    8.10 +
    8.11  setup \<open>KEStore_Elems.add_pbts
    8.12    [(Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
    8.13      (Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty

     9.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Jun 10 12:23:57 2021 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Jun 10 12:48:50 2021 +0200
     9.3 @@ -23,8 +23,6 @@
     9.4    lin_isolate_div:   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
     9.5  
     9.6  ML \<open>
     9.7 -val thy = @{theory};
     9.8 -
     9.9  val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
    9.10    Rule_Set.append_rules "LinEq_prls" Rule_Set.empty 
    9.11  	     [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),

    10.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Thu Jun 10 12:23:57 2021 +0200
    10.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Thu Jun 10 12:48:50 2021 +0200
    10.3 @@ -16,9 +16,6 @@
    10.4    equality_power:  "((a log b) = c) = (a \<up> (a log b) = a \<up> c)" and
    10.5    exp_invers_log:  "a \<up> (a log b) = b"
    10.6  
    10.7 -ML \<open>
    10.8 -val thy = @{theory};
    10.9 -\<close>
   10.10  (** problems **)
   10.11  setup \<open>KEStore_Elems.add_pbts
   10.12    [(Problem.prep_input @{theory} "pbl_test_equ_univ_log" [] Problem.id_empty

    11.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Thu Jun 10 12:23:57 2021 +0200
    11.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Thu Jun 10 12:48:50 2021 +0200
    11.3 @@ -177,7 +177,6 @@
    11.4  
    11.5  subsection \<open>auxiliary functions\<close>
    11.6  ML \<open>
    11.7 -val thy = @{theory};
    11.8  val poly_consts =
    11.9    ["Groups.plus_class.plus", "Groups.minus_class.minus",
   11.10    "Rings.divide_class.divide", "Groups.times_class.times",
   11.11 @@ -512,7 +511,7 @@
   11.12  end;(*local*)
   11.13  
   11.14  Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
   11.15 -[("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false thy)]);
   11.16 +[("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]);
   11.17  \<close>
   11.18  
   11.19  subsection \<open>predicates\<close>
   11.20 @@ -1009,7 +1008,7 @@
   11.21    (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
   11.22  val order_add_mult = 
   11.23    Rule_Def.Repeat{id = "order_add_mult", preconds = [], 
   11.24 -      rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
   11.25 +      rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
   11.26        erls = Rule_Set.empty,srls = Rule_Set.Empty,
   11.27        calc = [], errpatts = [],
   11.28        rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
   11.29 @@ -1029,7 +1028,7 @@
   11.30    (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
   11.31  val order_mult = 
   11.32    Rule_Def.Repeat{id = "order_mult", preconds = [], 
   11.33 -      rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
   11.34 +      rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
   11.35        erls = Rule_Set.empty,srls = Rule_Set.Empty,
   11.36        calc = [], errpatts = [],
   11.37        rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
   11.38 @@ -1054,8 +1053,8 @@
   11.39  	  prepat = 
   11.40            (* ?p matched with the current term gives an environment,
   11.41               which evaluates (the instantiated) "?p is_multUnordered" to true *)
   11.42 -	  [([TermC.parse_patt thy "?p is_multUnordered"], 
   11.43 -             TermC.parse_patt thy "?p :: real")],
   11.44 +	  [([TermC.parse_patt \<^theory> "?p is_multUnordered"], 
   11.45 +             TermC.parse_patt \<^theory> "?p :: real")],
   11.46  	  rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
   11.47  	  erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
   11.48  			    [Rule.Eval ("Poly.is_multUnordered", 

    12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Thu Jun 10 12:23:57 2021 +0200
    12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Thu Jun 10 12:48:50 2021 +0200
    12.3 @@ -319,8 +319,6 @@
    12.4    separate_1_bdv_n:       "bdv \<up> n / b = (1 / b) * bdv \<up> n"
    12.5  
    12.6  ML \<open>
    12.7 -val thy = @{theory};
    12.8 -
    12.9  (*-------------------------rulse-------------------------*)
   12.10  val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
   12.11    Rule_Set.append_rules "PolyEq_prls" Rule_Set.empty 

    13.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Jun 10 12:23:57 2021 +0200
    13.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Jun 10 12:48:50 2021 +0200
    13.3 @@ -105,8 +105,6 @@
    13.4    klammer_minus_mult:          "(b - c) * a = b * a - c * a"
    13.5  
    13.6  ML \<open>
    13.7 -val thy = @{theory};
    13.8 -
    13.9  (** eval functions **)
   13.10  
   13.11  (*. get the identifier from specific monomials; see fun ist_monom .*)

    14.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Thu Jun 10 12:23:57 2021 +0200
    14.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Thu Jun 10 12:48:50 2021 +0200
    14.3 @@ -50,8 +50,6 @@
    14.4  
    14.5  subsection \<open>predicates\<close>
    14.6  ML \<open>
    14.7 -val thy = @{theory};
    14.8 -
    14.9  (*-------------------------functions-----------------------*)
   14.10  (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
   14.11  fun is_rateqation_in t v = 

    15.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Thu Jun 10 12:23:57 2021 +0200
    15.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Jun 10 12:48:50 2021 +0200
    15.3 @@ -385,7 +385,7 @@
    15.4  \<close>
    15.5  
    15.6  section \<open>Embed cancellation and addition into rewriting\<close>
    15.7 -ML \<open>val thy = @{theory}\<close>
    15.8 +
    15.9  subsection \<open>Rulesets and predicate for embedding\<close>
   15.10  ML \<open>
   15.11  (* evaluates conditions in calculate_Rational *)
   15.12 @@ -510,7 +510,7 @@
   15.13  
   15.14  val cancel_p = 
   15.15    Rule_Set.Rrls {id = "cancel_p", prepat = [],
   15.16 -	rew_ord=("ord_make_polynomial", ord_make_polynomial false thy),
   15.17 +	rew_ord=("ord_make_polynomial", ord_make_polynomial false \<^theory>),
   15.18  	erls = rational_erls, 
   15.19  	calc = 
   15.20  	  [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
   15.21 @@ -519,10 +519,10 @@
   15.22  	  ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
   15.23      errpatts = [],
   15.24  	scr =
   15.25 -	  Rule.Rfuns {init_state  = init_state thy Atools_erls ro,
   15.26 -		normal_form = cancel_p_ thy, 
   15.27 -		locate_rule = locate_rule thy Atools_erls ro,
   15.28 -		next_rule   = next_rule thy Atools_erls ro,
   15.29 +	  Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
   15.30 +		normal_form = cancel_p_ \<^theory>, 
   15.31 +		locate_rule = locate_rule \<^theory> Atools_erls ro,
   15.32 +		next_rule   = next_rule \<^theory> Atools_erls ro,
   15.33  		attach_form = attach_form}}
   15.34  (**)end(* local cancel_p *)
   15.35  \<close>
   15.36 @@ -568,9 +568,9 @@
   15.37      end
   15.38    | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
   15.39  
   15.40 -val pat0 = TermC.parse_patt thy "?r/?s+?u/?v :: real";
   15.41 -val pat1 = TermC.parse_patt thy "?r/?s+?u    :: real";
   15.42 -val pat2 = TermC.parse_patt thy "?r   +?u/?v :: real";
   15.43 +val pat0 = TermC.parse_patt \<^theory> "?r/?s+?u/?v :: real";
   15.44 +val pat1 = TermC.parse_patt \<^theory> "?r/?s+?u    :: real";
   15.45 +val pat2 = TermC.parse_patt \<^theory> "?r   +?u/?v :: real";
   15.46  val prepat = [([@{term True}], pat0),
   15.47  	      ([@{term True}], pat1),
   15.48  	      ([@{term True}], pat2)];
   15.49 @@ -578,17 +578,17 @@
   15.50  
   15.51  val add_fractions_p =
   15.52    Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
   15.53 -    rew_ord = ("ord_make_polynomial", ord_make_polynomial false thy),
   15.54 +    rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
   15.55      erls = rational_erls,
   15.56      calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
   15.57        ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
   15.58        ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
   15.59        ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
   15.60      errpatts = [],
   15.61 -    scr = Rule.Rfuns {init_state  = init_state thy Atools_erls ro,
   15.62 -      normal_form = add_fraction_p_ thy,
   15.63 -      locate_rule = locate_rule thy Atools_erls ro,
   15.64 -      next_rule   = next_rule thy Atools_erls ro,
   15.65 +    scr = Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
   15.66 +      normal_form = add_fraction_p_ \<^theory>,
   15.67 +      locate_rule = locate_rule \<^theory> Atools_erls ro,
   15.68 +      next_rule   = next_rule \<^theory> Atools_erls ro,
   15.69        attach_form = attach_form}}
   15.70  (**)end(*local add_fractions_p *)
   15.71  \<close>

    16.1 --- a/src/Tools/isac/Knowledge/Root.thy	Thu Jun 10 12:23:57 2021 +0200
    16.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Thu Jun 10 12:48:50 2021 +0200
    16.3 @@ -42,8 +42,6 @@
    16.4    real_root_negative:      "a <  0 ==> (x  \<up>  2 = a) = False"
    16.5  
    16.6  ML \<open>
    16.7 -val thy = @{theory};
    16.8 -
    16.9  (*-------------------------functions---------------------*)
   16.10  (*evaluation square-root over the integers*)
   16.11  fun eval_sqrt (_ : string) (_ : string) (t as 
   16.12 @@ -191,7 +189,7 @@
   16.13  
   16.14  val make_rooteq = prep_rls'(
   16.15    Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list, 
   16.16 -      rew_ord = ("sqrt_right", sqrt_right false thy),
   16.17 +      rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
   16.18        erls = Atools_erls, srls = Rule_Set.Empty,
   16.19        calc = [], errpatts = [],
   16.20        rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),			

    17.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Thu Jun 10 12:23:57 2021 +0200
    17.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Thu Jun 10 12:48:50 2021 +0200
    17.3 @@ -107,8 +107,6 @@
    17.4  
    17.5  subsection \<open>predicates\<close>
    17.6  ML \<open>
    17.7 -val thy = @{theory};
    17.8 -
    17.9  (* true if bdv is under sqrt of a Equation*)
   17.10  fun is_rootTerm_in t v = 
   17.11    let 

    18.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Thu Jun 10 12:23:57 2021 +0200
    18.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Thu Jun 10 12:48:50 2021 +0200
    18.3 @@ -6,8 +6,6 @@
    18.4  theory RootRat imports Root Rational begin
    18.5  
    18.6  ML \<open>
    18.7 -val thy = @{theory};
    18.8 -
    18.9  val rootrat_erls = 
   18.10    Rule_Set.merge "rootrat_erls" Root_erls
   18.11      (Rule_Set.merge "" rational_erls

    19.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Jun 10 12:23:57 2021 +0200
    19.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Jun 10 12:48:50 2021 +0200
    19.3 @@ -33,8 +33,6 @@
    19.4  
    19.5  subsection \<open>predicates\<close>
    19.6  ML \<open>
    19.7 -val thy = @{theory};
    19.8 -
    19.9  (* true if denominator contains (sq)root in + or - term
   19.10     1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
   19.11     if false then (term)^2 contains no (sq)root *)

    20.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Thu Jun 10 12:23:57 2021 +0200
    20.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Thu Jun 10 12:48:50 2021 +0200
    20.3 @@ -20,9 +20,6 @@
    20.4    Simplify    :: "real => real"  (*"Simplify (1+2a+3+4a)*)
    20.5    Vereinfache :: "real => real"  (*"Vereinfache (1+2a+3+4a)*)
    20.6  
    20.7 -ML \<open>
    20.8 -val thy = @{theory};
    20.9 -\<close>
   20.10  (** problems **)
   20.11  setup \<open>KEStore_Elems.add_pbts
   20.12    [(Problem.prep_input @{theory} "pbl_simp" [] Problem.id_empty

    21.1 --- a/src/Tools/isac/Knowledge/Test.thy	Thu Jun 10 12:23:57 2021 +0200
    21.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Thu Jun 10 12:48:50 2021 +0200
    21.3 @@ -248,8 +248,6 @@
    21.4  
    21.5  section \<open>eval functions\<close>
    21.6  ML \<open>
    21.7 -val thy = @{theory};
    21.8 -
    21.9  (** evaluation of numerals and predicates **)
   21.10  
   21.11  (*does a term contain a root ?*)
   21.12 @@ -540,7 +538,7 @@
   21.13  	       Rule.Thm ("risolate_root_add",ThmC.numerals_to_Free @{thm risolate_root_add}),
   21.14  	       Rule.Thm ("risolate_root_mult",ThmC.numerals_to_Free @{thm risolate_root_mult}),
   21.15  	       Rule.Thm ("risolate_root_div",ThmC.numerals_to_Free @{thm risolate_root_div})       ],
   21.16 -      scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) 
   21.17 +      scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>)) 
   21.18        "empty_script")
   21.19        };
   21.20  
   21.21 @@ -556,7 +554,7 @@
   21.22  	 Rule.Thm ("constant_square",ThmC.numerals_to_Free @{thm constant_square}),
   21.23  	 Rule.Thm ("constant_mult_square",ThmC.numerals_to_Free @{thm constant_mult_square})
   21.24  	 ],
   21.25 -	scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) 
   21.26 +	scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>)) 
   21.27  			  "empty_script")
   21.28  	};      
   21.29  \<close>
   21.30 @@ -599,7 +597,7 @@
   21.31  ML \<open>
   21.32  Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
   21.33  [("termlessI", termlessI),
   21.34 - ("ord_make_polytest", ord_make_polytest false thy)
   21.35 + ("ord_make_polytest", ord_make_polytest false \<^theory>)
   21.36   ]);
   21.37  
   21.38  val make_polytest =
   21.39 @@ -1063,7 +1061,7 @@
   21.40      SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
   21.41          [''no_met'']) [BOOL e_e, REAL v_v])"
   21.42  setup \<open>KEStore_Elems.add_mets
   21.43 -    [MethodC.prep_input thy "met_test_norm_univ" [] MethodC.id_empty
   21.44 +    [MethodC.prep_input @{theory} "met_test_norm_univ" [] MethodC.id_empty
   21.45        (["Test", "norm_univar_equation"],
   21.46          [("#Given",["equality e_e", "solveFor v_v"]),
   21.47            ("#Where" ,[]), 
   21.48 @@ -1081,7 +1079,7 @@
   21.49      (Try (Calculate ''PLUS'')) #>         
   21.50      (Try (Calculate ''TIMES''))) t_t)"
   21.51  setup \<open>KEStore_Elems.add_mets
   21.52 -    [MethodC.prep_input thy "met_test_intsimp" [] MethodC.id_empty
   21.53 +    [MethodC.prep_input @{theory} "met_test_intsimp" [] MethodC.id_empty
   21.54        (["Test", "intsimp"],
   21.55          [("#Given" ,["intTestGiven t_t"]),
   21.56            ("#Where" ,[]),

    22.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml	Thu Jun 10 12:23:57 2021 +0200
    22.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml	Thu Jun 10 12:48:50 2021 +0200
    22.3 @@ -232,8 +232,8 @@
    22.4  "----------- Pattern.match ------------------------------";
    22.5  "----------- Pattern.match ------------------------------";
    22.6  "----------- Pattern.match ------------------------------";
    22.7 - val t = (Thm.term_of o the o (TermC.parse thy)) "3 * x\<up>2 = (1::real)";
    22.8 - val pat = (TermC.free2var o Thm.term_of o the o (TermC.parse thy)) "a * b\<up>2 = (c::real)";
    22.9 + val t = (Thm.term_of o the o (TermC.parse \<^theory>)) "3 * x\<up>2 = (1::real)";
   22.10 + val pat = (TermC.free2var o Thm.term_of o the o (TermC.parse \<^theory>)) "a * b\<up>2 = (c::real)";
   22.11   (*        ! \<up>  \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*)
   22.12   val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty);
   22.13  (*default_print_depth 3; 999*) insts;