1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sat Jun 12 18:06:27 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sat Jun 12 18:22:07 2021 +0200
     1.3 @@ -660,11 +660,9 @@
     1.4  	       (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
     1.5  		     and does not commute a / b * c  \<up>  2 !*)
     1.6  	       
     1.7 -	       Rule.Thm ("divide_divide_eq_right", 
     1.8 -                     ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
     1.9 +	       \<^rule_thm>\<open>divide_divide_eq_right\<close>,
    1.10  	       (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
    1.11 -	       Rule.Thm ("divide_divide_eq_left",
    1.12 -                     ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
    1.13 +	       \<^rule_thm>\<open>divide_divide_eq_left\<close>,
    1.14  	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
    1.15  	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
    1.16  	       ],