equal
deleted
inserted
replaced
123 qed "h_f_g_eq"; |
123 qed "h_f_g_eq"; |
124 |
124 |
125 |
125 |
126 (** A sequence of proof steps borrowed from Provers/split_paired_all.ML **) |
126 (** A sequence of proof steps borrowed from Provers/split_paired_all.ML **) |
127 |
127 |
128 val cT = TFree ("'c", ["term"]); |
128 val cT = TFree ("'c", HOLogic.typeS); |
129 |
129 |
130 (* "PROP P x == PROP P (h (f x, g x))" *) |
130 (* "PROP P x == PROP P (h (f x, g x))" *) |
131 val lemma1 = Thm.combination |
131 val lemma1 = Thm.combination |
132 (Thm.reflexive (cterm_of (sign_of thy) (Free ("P", cT --> propT)))) |
132 (Thm.reflexive (cterm_of (sign_of thy) (Free ("P", cT --> propT)))) |
133 (Drule.unvarify (h_f_g_eq RS sym RS eq_reflection)); |
133 (Drule.unvarify (h_f_g_eq RS sym RS eq_reflection)); |