| author | Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> |
| Mon, 27 Jan 2014 21:49:27 +0100 | |
| changeset 55359 | 73dc85c025ab |
| parent 52156 | aa0884017d48 |
| child 59410 | 2cbb98890190 |
| permissions | -rw-r--r-- |
1 theory Thy_2b imports Thy_1 begin
3 ML {* val test_list_rls =
4 append_rls "test_list_rls" e_rls [Thm ("False_def", @{thm False_def})] *}
6 setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
7 test_list_rls))] *}
8 ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset',
9 [("test_list_rls", test_list_rls)])*)
10 *}
12 end