equal
deleted
inserted
replaced
48 |
48 |
49 locale test = fixes x y :: 'a assumes eq: "x = y" |
49 locale test = fixes x y :: 'a assumes eq: "x = y" |
50 begin |
50 begin |
51 |
51 |
52 ML \<open> |
52 ML \<open> |
53 \<^simproc_setup>\<open>foo (x) = \<open>fn _ => fn _ => fn _ => SOME @{thm eq}\<close> |
53 \<^simproc_setup>\<open>foo (x) = |
|
54 \<open>fn phi => fn _ => fn _ => SOME (Morphism.thm phi @{thm eq})\<close> |
54 identifier test_axioms\<close> |
55 identifier test_axioms\<close> |
55 \<close> |
56 \<close> |
56 |
57 |
57 end |
58 end |
58 |
59 |