equal
deleted
inserted
replaced
178 apply (lem p1) |
178 apply (lem p1) |
179 apply safe |
179 apply safe |
180 apply (tactic {* |
180 apply (tactic {* |
181 REPEAT (rtac @{thm cut} 1 THEN |
181 REPEAT (rtac @{thm cut} 1 THEN |
182 DEPTH_SOLVE_1 |
182 DEPTH_SOLVE_1 |
183 (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN |
183 (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN |
184 Cla.safe_tac @{context} 1) *}) |
184 Cla.safe_tac @{context} 1) *}) |
185 done |
185 done |
186 |
186 |
187 lemma conj_cong: |
187 lemma conj_cong: |
188 assumes p1: "|- P <-> P'" |
188 assumes p1: "|- P <-> P'" |
191 apply (lem p1) |
191 apply (lem p1) |
192 apply safe |
192 apply safe |
193 apply (tactic {* |
193 apply (tactic {* |
194 REPEAT (rtac @{thm cut} 1 THEN |
194 REPEAT (rtac @{thm cut} 1 THEN |
195 DEPTH_SOLVE_1 |
195 DEPTH_SOLVE_1 |
196 (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN |
196 (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN |
197 Cla.safe_tac @{context} 1) *}) |
197 Cla.safe_tac @{context} 1) *}) |
198 done |
198 done |
199 |
199 |
200 lemma eq_sym_conv: "|- (x=y) <-> (y=x)" |
200 lemma eq_sym_conv: "|- (x=y) <-> (y=x)" |
201 by (fast add!: subst) |
201 by (fast add!: subst) |