equal
deleted
inserted
replaced
430 locale foo = |
430 locale foo = |
431 fixes A |
431 fixes A |
432 assumes A : "A" |
432 assumes A : "A" |
433 begin |
433 begin |
434 |
434 |
435 local_setup |
435 declaration \<open>fn phi => Data.put (Morphism.fact phi @{thms A})\<close> |
436 \<open>Local_Theory.declaration {pervasive = false, syntax = false, pos = \<^here>} |
|
437 (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close> |
|
438 |
436 |
439 lemma A by dynamic_thms_test |
437 lemma A by dynamic_thms_test |
440 |
438 |
441 end |
439 end |
442 |
440 |