src/HOL/Import/HOL4Compat.thy
changeset 23389 aaca6a8e5414
parent 20432 07ec57376051
child 29044 45dfd04a972e
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Thu Jun 14 18:33:29 2007 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Thu Jun 14 18:33:31 2007 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4      fix k
     1.5      show "!q. q + k = m \<longrightarrow> P q"
     1.6      proof (induct k,simp_all)
     1.7 -      show "P m" .
     1.8 +      show "P m" by fact
     1.9      next
    1.10        fix k
    1.11        assume ind: "!q. q + k = m \<longrightarrow> P q"
    1.12 @@ -406,7 +406,7 @@
    1.13    assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
    1.14    show "P l"
    1.15    proof (induct l)
    1.16 -    show "P []" .
    1.17 +    show "P []" by fact
    1.18    next
    1.19      fix h t
    1.20      assume "P t"