Put freeze into the signature TACTIC for export
authorlcp
Sat Mar 11 11:58:21 1995 +0100 (1995-03-11)
changeset 947812ccc91bfa0
parent 946 c0f4ae3fda92
child 948 3647161d15d3
Put freeze into the signature TACTIC for export
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Fri Mar 10 10:20:18 1995 +0100
     1.2 +++ b/src/Pure/tactic.ML	Sat Mar 11 11:58:21 1995 +0100
     1.3 @@ -45,6 +45,7 @@
     1.4    val fold_tac: thm list -> tactic
     1.5    val forward_tac: thm list -> int -> tactic   
     1.6    val forw_inst_tac: (string*string)list -> thm -> int -> tactic
     1.7 +  val freeze: thm -> thm   
     1.8    val is_fact: thm -> bool
     1.9    val lessb: (bool * thm) * (bool * thm) -> bool
    1.10    val lift_inst_rule: thm * int * (string*string)list * thm -> thm
    1.11 @@ -99,7 +100,7 @@
    1.12  fun string_of (a,0) = a
    1.13    | string_of (a,i) = a ^ "_" ^ string_of_int i;
    1.14  
    1.15 -(*convert all Vars in a theorem to Frees -- export??*)
    1.16 +(*convert all Vars in a theorem to Frees*)
    1.17  fun freeze th =
    1.18    let val fth = freezeT th
    1.19        val {prop,sign,...} = rep_thm fth