| 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-- |
| neuper@52146 | 1 |
theory Thy_2 imports Thy_1 begin |
| neuper@48809 | 2 |
|
| neuper@52139 | 3 |
ML {* val test_list_rls =
|
| neuper@52139 | 4 |
append_rls "test_list_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})] *}
|
| neuper@52139 | 5 |
|
| s1210629013@55359 | 6 |
setup {* Test_KEStore_Elems.add_rlss
|
| neuper@52146 | 7 |
[("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*)
|
| neuper@52139 | 8 |
test_list_rls))] *} |
| neuper@52139 | 9 |
|
| neuper@52156 | 10 |
ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset',
|
| neuper@52156 | 11 |
[("test_list_rls", test_list_rls)])*)
|
| neuper@52156 | 12 |
*} |
| neuper@48809 | 13 |
|
| neuper@48794 | 14 |
end |