src/Tools/isac/Knowledge/Test.thy
changeset 60289 a7b88fc19a92
parent 60286 31efa1b39a20
child 60290 bb4e8b01b072
     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>