author | wenzelm |
Mon, 27 Oct 1997 16:01:53 +0100 | |
changeset 4013 | 9ffb96bd2924 |
parent 4012 | 6adc18bd0009 |
child 4014 | df6cd80b6387 |
--- a/src/Pure/pure_thy.ML Mon Oct 27 15:57:50 1997 +0100 +++ b/src/Pure/pure_thy.ML Mon Oct 27 16:01:53 1997 +0100 @@ -9,7 +9,6 @@ sig val store_thms: (bstring * thm) list -> theory -> theory (*DESTRUCTIVE*) val store_thmss: (bstring * thm list) list -> theory -> theory (*DESTRUCTIVE*) - val store_thm: theory -> (bstring * thm) -> thm (*DESTRUCTIVE*) val smart_store_thm: (bstring * thm) -> thm (*DESTRUCTIVE*) val get_thm: theory -> xstring -> thm val get_thms: theory -> xstring -> thm list