equal
deleted
inserted
replaced
862 |
862 |
863 ML {* |
863 ML {* |
864 structure Hypsubst = HypsubstFun( |
864 structure Hypsubst = HypsubstFun( |
865 struct |
865 struct |
866 structure Simplifier = Simplifier |
866 structure Simplifier = Simplifier |
867 val dest_eq = HOLogic.dest_eq_typ |
867 val dest_eq = HOLogic.dest_eq |
868 val dest_Trueprop = HOLogic.dest_Trueprop |
868 val dest_Trueprop = HOLogic.dest_Trueprop |
869 val dest_imp = HOLogic.dest_imp |
869 val dest_imp = HOLogic.dest_imp |
870 val eq_reflection = HOL.eq_reflection |
870 val eq_reflection = HOL.eq_reflection |
871 val rev_eq_reflection = HOL.def_imp_eq |
871 val rev_eq_reflection = HOL.def_imp_eq |
872 val imp_intr = HOL.impI |
872 val imp_intr = HOL.impI |