| changeset 24976 | 821628d16552 |
| parent 24241 | 424cb8b5e5b4 |
| child 26424 | a6cad32a27b0 |
--- a/src/Pure/conjunction.ML Thu Oct 11 18:58:34 2007 +0200 +++ b/src/Pure/conjunction.ML Thu Oct 11 19:10:17 2007 +0200 @@ -69,7 +69,7 @@ val ABC = read_prop "A ==> B ==> C"; val A_B = read_prop "A && B"; -val conjunction_def = Drule.unvarify ProtoPure.conjunction_def; +val conjunction_def = Thm.unvarify ProtoPure.conjunction_def; fun conjunctionD which = Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP