clarified theory context: avoid global "val thy = ..." hanging around (left-over from Isabelle2005), which is apt to various pitfalls;
1 (* Title: collecting all knowledge for Root and Rational
2 Author: Richard Lang 02.10 last change by: rlang date: 02.10.20
3 (c) due to copyright terms
6 theory RootRat imports Root Rational begin
10 Rule_Set.merge "rootrat_erls" Root_erls
11 (Rule_Set.merge "" rational_erls
12 (Rule_Set.append_rules "" Rule_Set.empty []));
14 (*.calculate numeral groundterms.*)
15 val calculate_RootRat =
16 Rule_Set.append_rules "calculate_RootRat" calculate_Rational
17 [Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
18 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
19 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
21 Rule.Thm ("sym_real_mult_minus1",ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})),
22 (* "- z1 = -1 * z1" *)
23 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")
26 val prep_rls' = Auto_Prog.prep_rls @{theory};
29 rootrat_erls = \<open>prep_rls' rootrat_erls\<close> and
30 calculate_RootRat = \<open>prep_rls' calculate_RootRat\<close>