1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Sun Apr 25 12:03:49 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Sun Apr 25 12:49:37 2021 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    antiDerivative      :: "real => una"
     1.5    antiDerivativeName  :: "(real => real) => una"
     1.6  
     1.7 -  (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
     1.8 +  (*the CAS-command, eg. "Integrate (2*x \<up> 3, x)"*)
     1.9    Integrate           :: "[real * real] => real"
    1.10  
    1.11  axiomatization where
    1.12 @@ -193,7 +193,7 @@
    1.13  	       Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.14  	      
    1.15  	       Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
    1.16 -		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
    1.17 +		(*"(?a / ?b)  \<up>  ?n = ?a  \<up>  ?n / ?b  \<up>  ?n"*)
    1.18  	       ],
    1.19        scr = Rule.Empty_Prog
    1.20        }),
    1.21 @@ -234,7 +234,7 @@
    1.22  		Rule.Thm ("separate_1_bdv",  ThmC.numerals_to_Free @{thm separate_1_bdv}),
    1.23  		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.24  		Rule.Thm ("separate_1_bdv_n",  ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
    1.25 -			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
    1.26 +			  (*"?bdv  \<up>  ?n / ?b = 1 / ?b * ?bdv  \<up>  ?n"*)
    1.27  			  *****Rule.Thm ("add_divide_distrib", 
    1.28  			  ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
    1.29  			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
    1.30 @@ -287,7 +287,7 @@
    1.31  * 			  Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
    1.32  * 			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.33  * 			  Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
    1.34 -* 			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
    1.35 +* 			  (*"?bdv  \<up>  ?n / ?b = 1 / ?b * ?bdv  \<up>  ?n"*)
    1.36  * 			  Rule.Thm ("add_divide_distrib", 
    1.37  * 				  ThmC.numerals_to_Free @{thm add_divide_distrib})
    1.38  * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)