src/Pure/Thy/thm_database.ML
changeset 5346 bc9748ad8491
parent 5155 21177b8a4d7f
child 5744 9e73738f2307
     1.1 --- a/src/Pure/Thy/thm_database.ML	Wed Aug 19 17:05:00 1998 +0200
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Thu Aug 20 09:25:59 1998 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature THM_DATABASE =
     1.6  sig
     1.7 +  val ml_store_thm: string * thm -> unit
     1.8    val store_thm: string * thm -> thm
     1.9    val qed_thm: thm option ref
    1.10    val bind_thm: string * thm -> unit