changeset 2326 | 6df4488339e4 |
parent 1969 | af6d59e26dd9 |
child 2563 | e908e2716f3a |
2325:ea8a1fc512e6 | 2326:6df4488339e4 |
---|---|
18 created by init_thy_reader.*) |
18 created by init_thy_reader.*) |
19 fun qed_spec_mp name = |
19 fun qed_spec_mp name = |
20 let val thm = normalize_thm [RSspec,RSmp] (result()) |
20 let val thm = normalize_thm [RSspec,RSmp] (result()) |
21 in bind_thm(name, thm) end; |
21 in bind_thm(name, thm) end; |
22 |
22 |
23 use_thy "Shared"; |
23 use_thy "Message"; |
24 |
24 |