1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Sat Jun 12 18:06:27 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Sat Jun 12 18:22:07 2021 +0200
     1.3 @@ -223,67 +223,49 @@
     1.4              (* sqrt a sqrt b -> sqrt(ab) *)
     1.5         \<^rule_thm>\<open>sqrt_times_root_2\<close>,
     1.6              (* a sqrt b sqrt c -> a sqrt(bc) *)
     1.7 -       Rule.Thm("sqrt_square_equation_both_1",
     1.8 -           ThmC.numerals_to_Free @{thm sqrt_square_equation_both_1}),
     1.9 +       \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>,
    1.10         (* (sqrt a + sqrt b  = sqrt c + sqrt d) -> 
    1.11              (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
    1.12 -       Rule.Thm("sqrt_square_equation_both_2",
    1.13 -            ThmC.numerals_to_Free @{thm sqrt_square_equation_both_2}),
    1.14 +       \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>,
    1.15         (* (sqrt a - sqrt b  = sqrt c + sqrt d) -> 
    1.16              (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
    1.17 -       Rule.Thm("sqrt_square_equation_both_3",
    1.18 -            ThmC.numerals_to_Free @{thm sqrt_square_equation_both_3}),
    1.19 +       \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>,
    1.20         (* (sqrt a + sqrt b  = sqrt c - sqrt d) -> 
    1.21              (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
    1.22 -       Rule.Thm("sqrt_square_equation_both_4",
    1.23 -            ThmC.numerals_to_Free @{thm sqrt_square_equation_both_4}),
    1.24 +       \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>,
    1.25         (* (sqrt a - sqrt b  = sqrt c - sqrt d) -> 
    1.26              (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
    1.27 -       Rule.Thm("sqrt_isolate_l_add1",
    1.28 -            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add1}), 
    1.29 +       \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>, 
    1.30         (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
    1.31 -       Rule.Thm("sqrt_isolate_l_add2",
    1.32 -            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add2}), 
    1.33 +       \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, 
    1.34         (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)
    1.35 -       Rule.Thm("sqrt_isolate_l_add3",
    1.36 -            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add3}), 
    1.37 +       \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, 
    1.38         (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
    1.39 -       Rule.Thm("sqrt_isolate_l_add4",
    1.40 -            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add4}), 
    1.41 +       \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, 
    1.42         (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
    1.43 -       Rule.Thm("sqrt_isolate_l_add5",
    1.44 -            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add5}), 
    1.45 +       \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, 
    1.46         (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
    1.47 -       Rule.Thm("sqrt_isolate_l_add6",
    1.48 -            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}), 
    1.49 +       \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, 
    1.50         (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
    1.51         (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
    1.52           (* b*sqrt(x) = d sqrt(x) d/b *)
    1.53 -       Rule.Thm("sqrt_isolate_r_add1",
    1.54 -            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}),
    1.55 +       \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
    1.56         (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
    1.57 -       Rule.Thm("sqrt_isolate_r_add2",
    1.58 -            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add2}),
    1.59 +       \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
    1.60         (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)
    1.61 -       Rule.Thm("sqrt_isolate_r_add3",
    1.62 -            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add3}),
    1.63 +       \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
    1.64         (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
    1.65 -       Rule.Thm("sqrt_isolate_r_add4",
    1.66 -            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add4}),
    1.67 +       \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
    1.68         (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
    1.69 -       Rule.Thm("sqrt_isolate_r_add5",
    1.70 -            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add5}),
    1.71 +       \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
    1.72         (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
    1.73 -       Rule.Thm("sqrt_isolate_r_add6",
    1.74 -            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}),
    1.75 +       \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
    1.76         (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
    1.77         (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
    1.78           (* a=e*sqrt(x) -> a/e = sqrt(x) *)
    1.79 -       Rule.Thm("sqrt_square_equation_left_1",
    1.80 -            ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}),   
    1.81 +       \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,   
    1.82         (* sqrt(x)=b -> x=b^2 *)
    1.83 -       Rule.Thm("sqrt_square_equation_left_2",
    1.84 -            ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}),   
    1.85 +       \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,   
    1.86         (* c*sqrt(x)=b -> c^2*x=b^2 *)
    1.87         \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,  
    1.88  	      (* c/sqrt(x)=b -> c^2/x=b^2 *)