equal
deleted
inserted
replaced
320 \<longrightarrow> (\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> q(y,x))" |
320 \<longrightarrow> (\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> q(y,x))" |
321 by blast |
321 by blast |
322 |
322 |
323 text \<open> |
323 text \<open> |
324 Other proofs: Can use @{text auto}, which cheats by using rewriting! |
324 Other proofs: Can use @{text auto}, which cheats by using rewriting! |
325 Deepen_tac alone requires 253 secs. Or |
325 @{text Deepen_tac} alone requires 253 secs. Or |
326 by (mini_tac 1 THEN Deepen_tac 5 1) |
326 @{text \<open>by (mini_tac 1 THEN Deepen_tac 5 1)\<close>}. |
327 \<close> |
327 \<close> |
328 |
328 |
329 text\<open>44\<close> |
329 text\<open>44\<close> |
330 lemma |
330 lemma |
331 "(\<forall>x. f(x) \<longrightarrow> (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and> |
331 "(\<forall>x. f(x) \<longrightarrow> (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and> |