equal
deleted
inserted
replaced
82 Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP |
82 Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP |
83 Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B)); |
83 Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B)); |
84 |
84 |
85 in |
85 in |
86 |
86 |
87 val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1); |
87 val conjunctionD1 = |
88 val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2); |
88 Drule.store_standard_thm (Binding.make ("conjunctionD1", @{here})) (conjunctionD #1); |
|
89 |
|
90 val conjunctionD2 = |
|
91 Drule.store_standard_thm (Binding.make ("conjunctionD2", @{here})) (conjunctionD #2); |
89 |
92 |
90 val conjunctionI = |
93 val conjunctionI = |
91 Drule.store_standard_thm (Binding.name "conjunctionI") |
94 Drule.store_standard_thm (Binding.make ("conjunctionI", @{here})) |
92 (Drule.implies_intr_list [A, B] |
95 (Drule.implies_intr_list [A, B] |
93 (Thm.equal_elim |
96 (Thm.equal_elim |
94 (Thm.symmetric conjunction_def) |
97 (Thm.symmetric conjunction_def) |
95 (Thm.forall_intr C (Thm.implies_intr ABC |
98 (Thm.forall_intr C (Thm.implies_intr ABC |
96 (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B]))))); |
99 (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B]))))); |