src/HOL/cladata.ML
changeset 4223 f60e3d2c81d3
parent 4206 688050e83d89
child 4240 8ba60a4cd380
equal deleted inserted replaced
4222:d7573d6d0513 4223:f60e3d2c81d3
    19   val eq_reflection = eq_reflection
    19   val eq_reflection = eq_reflection
    20   val imp_intr = impI
    20   val imp_intr = impI
    21   val rev_mp = rev_mp
    21   val rev_mp = rev_mp
    22   val subst = subst
    22   val subst = subst
    23   val sym = sym
    23   val sym = sym
       
    24   val thin_refl = prove_goal HOL.thy 
       
    25 		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
    24   end;
    26   end;
    25 
    27 
    26 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    28 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    27 open Hypsubst;
    29 open Hypsubst;
    28 
    30