src/FOL/hypsubstdata.ML
changeset 9528 95852b4be214
parent 7355 4c43090659ca
child 12345 5d1436d1c268
equal deleted inserted replaced
9527:de95b5125580 9528:95852b4be214
     6     (*These destructors  Match!*)
     6     (*These destructors  Match!*)
     7   fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
     7   fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
     8   val dest_Trueprop = FOLogic.dest_Trueprop
     8   val dest_Trueprop = FOLogic.dest_Trueprop
     9   val dest_imp = FOLogic.dest_imp
     9   val dest_imp = FOLogic.dest_imp
    10   val eq_reflection = eq_reflection
    10   val eq_reflection = eq_reflection
       
    11   val rev_eq_reflection = meta_eq_to_obj_eq
    11   val imp_intr = impI
    12   val imp_intr = impI
    12   val rev_mp = rev_mp
    13   val rev_mp = rev_mp
    13   val subst = subst
    14   val subst = subst
    14   val sym = sym
    15   val sym = sym
    15   val thin_refl = prove_goal (the_context ())
    16   val thin_refl = prove_goal (the_context ())