equal
deleted
inserted
replaced
27 include BASIC_THM_DATABASE |
27 include BASIC_THM_DATABASE |
28 val qed_thms: thm list ref |
28 val qed_thms: thm list ref |
29 val ml_store_thm: string * thm -> unit |
29 val ml_store_thm: string * thm -> unit |
30 val ml_store_thms: string * thm list -> unit |
30 val ml_store_thms: string * thm list -> unit |
31 val is_ml_identifier: string -> bool |
31 val is_ml_identifier: string -> bool |
|
32 val ml_reserved: string list |
32 val print_thms_containing: theory -> term list -> unit |
33 val print_thms_containing: theory -> term list -> unit |
33 end; |
34 end; |
34 |
35 |
35 structure ThmDatabase: THM_DATABASE = |
36 structure ThmDatabase: THM_DATABASE = |
36 struct |
37 struct |