equal
deleted
inserted
replaced
29 use "domain/axioms.ML"; |
29 use "domain/axioms.ML"; |
30 use "domain/theorems.ML"; |
30 use "domain/theorems.ML"; |
31 use "domain/extender.ML"; |
31 use "domain/extender.ML"; |
32 use "domain/interface.ML"; |
32 use "domain/interface.ML"; |
33 |
33 |
34 init_thy_reader(); |
34 set_parser ThySyn.parse; |
35 |
35 |
36 fun qed_spec_mp name = |
36 fun qed_spec_mp name = |
37 let val thm = normalize_thm [RSspec,RSmp] (result()) |
37 let val thm = normalize_thm [RSspec,RSmp] (result()) |
38 in bind_thm(name, thm) end; |
38 in bind_thm(name, thm) end; |
39 |
39 |