src/HOL/Import/proof_kernel.ML
changeset 19068 04b302f2902d
parent 19067 c0321d7d6b3d
child 19264 61e775c03ed8
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 04:17:19 2006 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Feb 16 14:59:57 2006 +0100
     1.3 @@ -114,6 +114,7 @@
     1.4      val prin : term -> unit 
     1.5      val protect_factname : string -> string 
     1.6      val replay_protect_varname : string -> string -> unit
     1.7 +    val replay_add_dump : string -> theory -> theory
     1.8  end
     1.9  
    1.10  structure ProofKernel :> ProofKernel =
    1.11 @@ -128,6 +129,9 @@
    1.12  
    1.13  fun to_hol_thm th = HOLThm ([], th)
    1.14  
    1.15 +val replay_add_dump = add_dump
    1.16 +fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
    1.17 +
    1.18  datatype proof_info
    1.19    = Info of {disk_info: (string * string) option ref}
    1.20