1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -35,17 +35,17 @@
     1.4   	      Rule.Num_Calc ("Poly.is'_polyrat'_in", eval_is_polyrat_in ""),
     1.5  	      Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
     1.6  	      Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
     1.7 -	      Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
     1.8 -	      Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
     1.9 -	      Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
    1.10 -	      Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
    1.11 -	      Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
    1.12 -	      Rule.Thm ("or_false",TermC.num_str @{thm or_false})
    1.13 +	      Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
    1.14 +	      Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
    1.15 +	      Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
    1.16 +	      Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
    1.17 +	      Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
    1.18 +	      Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})
    1.19                ];
    1.20  (* ----- erls ----- *)
    1.21  val LinEq_crls = 
    1.22     Rule_Set.append_rules "LinEq_crls" poly_crls
    1.23 -   [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
    1.24 +   [Rule.Thm  ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
    1.25      (*		
    1.26       Don't use
    1.27       Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.28 @@ -56,7 +56,7 @@
    1.29  (* ----- crls ----- *)
    1.30  val LinEq_erls = 
    1.31     Rule_Set.append_rules "LinEq_erls" Poly_erls
    1.32 -   [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
    1.33 +   [Rule.Thm  ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
    1.34      (*		
    1.35       Don't use
    1.36       Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.37 @@ -75,7 +75,7 @@
    1.38         srls = Rule_Set.Empty, 
    1.39         calc = [], errpatts = [],
    1.40         rules = [
    1.41 -		Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
    1.42 +		Rule.Thm  ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1}),
    1.43  		Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.44  		Rule.Num_Calc ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
    1.45  		Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.46 @@ -99,11 +99,11 @@
    1.47       srls = Rule_Set.Empty,
    1.48       calc = [], errpatts = [],
    1.49       rules = [
    1.50 -	      Rule.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}), 
    1.51 +	      Rule.Thm("lin_isolate_add1",ThmC.numerals_to_Free @{thm lin_isolate_add1}), 
    1.52  	      (* a+bx=0 -> bx=-a *)
    1.53 -	      Rule.Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}), 
    1.54 +	      Rule.Thm("lin_isolate_add2",ThmC.numerals_to_Free @{thm lin_isolate_add2}), 
    1.55  	      (* a+ x=0 ->  x=-a *)
    1.56 -	      Rule.Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div})    
    1.57 +	      Rule.Thm("lin_isolate_div",ThmC.numerals_to_Free @{thm lin_isolate_div})    
    1.58  	      (*   bx=c -> x=c/b *)  
    1.59  	      ],
    1.60       scr = Rule.EmptyScr});