restored last version
authoroheimb
Wed Nov 12 12:34:43 1997 +0100 (1997-11-12)
changeset 4206688050e83d89
parent 4205 96632970d203
child 4207 061919f8da9c
restored last version
src/HOL/cladata.ML
     1.1 --- a/src/HOL/cladata.ML	Wed Nov 12 12:30:15 1997 +0100
     1.2 +++ b/src/HOL/cladata.ML	Wed Nov 12 12:34:43 1997 +0100
     1.3 @@ -26,9 +26,6 @@
     1.4  structure Hypsubst = HypsubstFun(Hypsubst_Data);
     1.5  open Hypsubst;
     1.6  
     1.7 -val thin_refl = prove_goal HOL.thy 
     1.8 -	"!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
     1.9 -
    1.10  (*** Applying ClassicalFun to create a classical prover ***)
    1.11  structure Classical_Data = 
    1.12    struct
    1.13 @@ -36,8 +33,7 @@
    1.14    val mp        = mp
    1.15    val not_elim  = notE
    1.16    val classical = classical
    1.17 -  val thin_refl = thin_refl
    1.18 -  val hyp_subst_tacs= [REPEAT_DETERM o ematch_tac [thin_refl] THEN' hyp_subst_tac]
    1.19 +  val hyp_subst_tacs=[hyp_subst_tac]
    1.20    end;
    1.21  
    1.22  structure Classical = ClassicalFun(Classical_Data);