1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sun Apr 25 12:03:49 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sun Apr 25 12:49:37 2021 +0200
     1.3 @@ -436,7 +436,7 @@
     1.4            (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
     1.5          
     1.6          Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),
     1.7 -          (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
     1.8 +          (*"(?a / ?b)  \<up>  ?n = ?a  \<up>  ?n / ?b  \<up>  ?n"*)
     1.9          
    1.10          Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),
    1.11            (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
    1.12 @@ -618,29 +618,29 @@
    1.13    Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.14        erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.15        rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
    1.16 -	       (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
    1.17 +	       (*"(r * s)  \<up>  n = r  \<up>  n * s  \<up>  n"*)
    1.18  	       Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
    1.19 -	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
    1.20 +	       (*"(a  \<up>  b)  \<up>  c = a  \<up>  (b * c)"*)
    1.21  	       Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
    1.22 -	       (*"r ^^^ 1 = r"*)
    1.23 +	       (*"r  \<up>  1 = r"*)
    1.24  	       Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
    1.25 -	       (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*)
    1.26 +	       (*"n is_even ==> (- r)  \<up>  n = r  \<up>  n" ?-->discard_minus?*)
    1.27  	       Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}),
    1.28 -	       (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*)
    1.29 +	       (*"Not (n is_even) ==> (- r)  \<up>  n = -1 * r  \<up>  n"*)
    1.30  	       
    1.31  	       (*----- collect atoms over * -----*)
    1.32  	       Rule.Thm ("realpow_two_atom",ThmC.numerals_to_Free @{thm realpow_two_atom}),	
    1.33 -	       (*"r is_atom ==> r * r = r ^^^ 2"*)
    1.34 +	       (*"r is_atom ==> r * r = r  \<up>  2"*)
    1.35  	       Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),		
    1.36 -	       (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*)
    1.37 +	       (*"r is_atom ==> r * r  \<up>  n = r  \<up>  (n + 1)"*)
    1.38  	       Rule.Thm ("realpow_addI_atom",ThmC.numerals_to_Free @{thm realpow_addI_atom}),
    1.39 -	       (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
    1.40 +	       (*"r is_atom ==> r  \<up>  n * r  \<up>  m = r  \<up>  (n + m)"*)
    1.41  
    1.42  	       (*----- distribute none-atoms -----*)
    1.43  	       Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
    1.44 -	       (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
    1.45 +	       (*"[| 1 < n; not(r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
    1.46  	       Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
    1.47 -	       (*"1 ^^^ n = 1"*)
    1.48 +	       (*"1  \<up>  n = 1"*)
    1.49  	       Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
    1.50  	       ],
    1.51        scr = Rule.Empty_Prog
    1.52 @@ -656,8 +656,8 @@
    1.53  	       (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
    1.54  	       otherwise inv.to a / b / c = ...*)
    1.55  	       Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
    1.56 -	       (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much
    1.57 -		     and does not commute a / b * c ^^^ 2 !*)
    1.58 +	       (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
    1.59 +		     and does not commute a / b * c  \<up>  2 !*)
    1.60  	       
    1.61  	       Rule.Thm ("divide_divide_eq_right", 
    1.62                       ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
    1.63 @@ -810,7 +810,7 @@
    1.64        Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.65        
    1.66        Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
    1.67 -      (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
    1.68 +      (*"(?a / ?b)  \<up>  ?n = ?a  \<up>  ?n / ?b  \<up>  ?n"*)
    1.69        ],
    1.70      scr = Rule.Empty_Prog});
    1.71