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/Import/HOL4Compat.thy
changeset 23389 aaca6a8e5414
parent 20432 07ec57376051
child 29044 45dfd04a972e 
--- a/src/HOL/Import/HOL4Compat.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -157,7 +157,7 @@
     fix k
     show "!q. q + k = m \<longrightarrow> P q"
     proof (induct k,simp_all)
-      show "P m" .
+      show "P m" by fact
     next
       fix k
       assume ind: "!q. q + k = m \<longrightarrow> P q"
@@ -406,7 +406,7 @@
   assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
   show "P l"
   proof (induct l)
-    show "P []" .
+    show "P []" by fact
   next
     fix h t
     assume "P t"
isabelle