src/FOL/ROOT.ML
changeset 4223 f60e3d2c81d3
parent 4222 d7573d6d0513
child 4349 50403e5a44c0
equal deleted inserted replaced
4222:d7573d6d0513 4223:f60e3d2c81d3
    32   val eq_reflection = eq_reflection
    32   val eq_reflection = eq_reflection
    33   val imp_intr = impI
    33   val imp_intr = impI
    34   val rev_mp = rev_mp
    34   val rev_mp = rev_mp
    35   val subst = subst
    35   val subst = subst
    36   val sym = sym
    36   val sym = sym
       
    37   val thin_refl = prove_goal IFOL.thy 
       
    38 		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
    37   end;
    39   end;
    38 
    40 
    39 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    41 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    40 open Hypsubst;
    42 open Hypsubst;
    41 
    43