1.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Jun 09 20:28:42 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Jun 10 11:54:20 2021 +0200
1.3 @@ -436,7 +436,7 @@
1.4 scr = Rule.Empty_Prog
1.5 };
1.6 \<close>
1.7 -setup_rule testerls = \<open>prep_rls' testerls\<close>
1.8 +rule_set_knowledge testerls = \<open>prep_rls' testerls\<close>
1.9
1.10 ML \<open>
1.11 (*make () dissappear*)
1.12 @@ -561,7 +561,7 @@
1.13 };
1.14 \<close>
1.15 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close>
1.16 -setup_rule
1.17 +rule_set_knowledge
1.18 Test_simplify = \<open>prep_rls' Test_simplify\<close> and
1.19 tval_rls = \<open>prep_rls' tval_rls\<close> and
1.20 isolate_root = \<open>prep_rls' isolate_root\<close> and
1.21 @@ -766,10 +766,10 @@
1.22 (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
1.23 };
1.24 \<close>
1.25 -setup_rule
1.26 +rule_set_knowledge
1.27 make_polytest = \<open>prep_rls' make_polytest\<close> and
1.28 expand_binomtest = \<open>prep_rls' expand_binomtest\<close>
1.29 -setup_rule
1.30 +rule_set_knowledge
1.31 norm_equation = \<open>prep_rls' norm_equation\<close> and
1.32 ac_plus_times = \<open>prep_rls' ac_plus_times\<close> and
1.33 rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close>