Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Isar_Examples/Higher_Order_Logic.thy
changeset 63532 b01154b74314
parent 62266 f4baefee5776
child 63585 f4a308fdf664 
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Wed Jul 20 21:26:11 2016 +0200
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Wed Jul 20 22:36:10 2016 +0200
@@ -82,7 +82,7 @@
   assumes "\<bottom>"
   shows A
 proof -
-  from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
+  from \<open>\<bottom>\<close> have "\<forall>A. A" by (simp only: false_def)
   then show A ..
 qed
 
@@ -108,7 +108,7 @@
   assumes "\<not> A" and A
   shows B
 proof -
-  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
+  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" by (simp only: not_def)
   from this and \<open>A\<close> have "\<bottom>" ..
   then show B ..
 qed
isabelle