equal
deleted
inserted
replaced
934 val not_intro_thm = Thm.symmetric not_elim_thm |
934 val not_intro_thm = Thm.symmetric not_elim_thm |
935 val abs_thm = @{thm ext} |
935 val abs_thm = @{thm ext} |
936 val trans_thm = @{thm trans} |
936 val trans_thm = @{thm trans} |
937 val symmetry_thm = @{thm sym} |
937 val symmetry_thm = @{thm sym} |
938 val eqmp_thm = @{thm iffD1} |
938 val eqmp_thm = @{thm iffD1} |
939 val eqimp_thm = @{thm HOL4Setup.eq_imp} |
939 val eqimp_thm = @{thm Importer.eq_imp} |
940 val comb_thm = @{thm cong} |
940 val comb_thm = @{thm cong} |
941 |
941 |
942 (* Beta-eta normalizes a theorem (only the conclusion, not the * |
942 (* Beta-eta normalizes a theorem (only the conclusion, not the * |
943 hypotheses!) *) |
943 hypotheses!) *) |
944 |
944 |