src/FOL/hypsubstdata.ML
changeset 21539 c5cf9243ad62
parent 21218 38013c3a77a2
child 27572 67cd6ed76446
equal deleted inserted replaced
21538:678299eac351 21539:c5cf9243ad62
     4 struct
     4 struct
     5   structure Simplifier = Simplifier
     5   structure Simplifier = Simplifier
     6   val dest_eq = FOLogic.dest_eq
     6   val dest_eq = FOLogic.dest_eq
     7   val dest_Trueprop = FOLogic.dest_Trueprop
     7   val dest_Trueprop = FOLogic.dest_Trueprop
     8   val dest_imp = FOLogic.dest_imp
     8   val dest_imp = FOLogic.dest_imp
     9   val eq_reflection = eq_reflection
     9   val eq_reflection = thm "eq_reflection"
    10   val rev_eq_reflection = meta_eq_to_obj_eq
    10   val rev_eq_reflection = thm "meta_eq_to_obj_eq"
    11   val imp_intr = impI
    11   val imp_intr = thm "impI"
    12   val rev_mp = rev_mp
    12   val rev_mp = thm "rev_mp"
    13   val subst = subst
    13   val subst = thm "subst"
    14   val sym = sym
    14   val sym = thm "sym"
    15   val thin_refl = prove_goal (the_context ()) "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
    15   val thin_refl = thm "thin_refl"
    16 end;
    16 end;
    17 
    17 
    18 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    18 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    19 open Hypsubst;
    19 open Hypsubst;