src/Pure/Thy/thm_database.ML
changeset 5346 bc9748ad8491
parent 5155 21177b8a4d7f
child 5744 9e73738f2307
equal deleted inserted replaced
5345:d7927fc7170d 5346:bc9748ad8491
     5 User level interface to thm database (see also Pure/pure_thy.ML).
     5 User level interface to thm database (see also Pure/pure_thy.ML).
     6 *)
     6 *)
     7 
     7 
     8 signature THM_DATABASE =
     8 signature THM_DATABASE =
     9 sig
     9 sig
       
    10   val ml_store_thm: string * thm -> unit
    10   val store_thm: string * thm -> thm
    11   val store_thm: string * thm -> thm
    11   val qed_thm: thm option ref
    12   val qed_thm: thm option ref
    12   val bind_thm: string * thm -> unit
    13   val bind_thm: string * thm -> unit
    13   val qed: string -> unit
    14   val qed: string -> unit
    14   val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
    15   val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit