22 preconds = [], rew_ord = ("termlessI", termlessI), erls = e_rls, |
22 preconds = [], rew_ord = ("termlessI", termlessI), erls = e_rls, |
23 srls = Erls, calc = [], errpatts = [], |
23 srls = Erls, calc = [], errpatts = [], |
24 rules = [Thm ("thm111", @{thm thm111}), |
24 rules = [Thm ("thm111", @{thm thm111}), |
25 Thm ("refl", @{thm refl}), Thm ("o_def", @{thm o_def})], |
25 Thm ("refl", @{thm refl}), Thm ("o_def", @{thm o_def})], |
26 scr = EmptyScr}; |
26 scr = EmptyScr}; |
|
27 |
|
28 val prep_rls' = prep_rls @{theory}; |
27 *} |
29 *} |
28 |
30 |
29 setup {* KEStore_Elems.add_rlss |
31 setup {* KEStore_Elems.add_rlss |
30 [("rls111", (Context.theory_name @{theory}, prep_rls rls111)), |
32 [("rls111", (Context.theory_name @{theory}, prep_rls' rls111)), |
31 ("rls222", (Context.theory_name @{theory}, prep_rls rls222))] *} |
33 ("rls222", (Context.theory_name @{theory}, prep_rls' rls222))] *} |
32 |
34 |
33 ML {* |
35 ML {* |
34 @{thm refl}; |
36 @{thm refl}; |
35 @{thm o_def}; |
37 @{thm o_def}; |
36 *} |
38 *} |