src/HOL/cladata.ML
changeset 4223 f60e3d2c81d3
parent 4206 688050e83d89
child 4240 8ba60a4cd380
     1.1 --- a/src/HOL/cladata.ML	Wed Nov 12 16:28:53 1997 +0100
     1.2 +++ b/src/HOL/cladata.ML	Wed Nov 12 18:58:50 1997 +0100
     1.3 @@ -21,6 +21,8 @@
     1.4    val rev_mp = rev_mp
     1.5    val subst = subst
     1.6    val sym = sym
     1.7 +  val thin_refl = prove_goal HOL.thy 
     1.8 +		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
     1.9    end;
    1.10  
    1.11  structure Hypsubst = HypsubstFun(Hypsubst_Data);