Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Mon, 18 Apr 2016 15:13:46 +0200
changeset 63013 37a74da77be7
parent 63012 75f488e15479
child 63014 6fff9774e088
tuned;
src/HOL/Eisbach/Examples.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Eisbach/Examples.thy	Mon Apr 18 14:47:27 2016 +0200
+++ b/src/HOL/Eisbach/Examples.thy	Mon Apr 18 15:13:46 2016 +0200
@@ -183,7 +183,7 @@
   apply prop_solver
   done
 
-lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow>  P z \<Longrightarrow> P y \<Longrightarrow> Q y"
+lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P z \<Longrightarrow> P y \<Longrightarrow> Q y"
   apply (solves \<open>guess_all, prop_solver\<close>)  \<comment> \<open>Try it without solve\<close>
   done
isabelle