src/HOL/Import/HOL4Compat.thy
changeset 32960 69916a850301
parent 32479 521cc9bf2958
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -166,19 +166,19 @@
     1.4        assume ind: "!q. q + k = m \<longrightarrow> P q"
     1.5        show "!q. Suc (q + k) = m \<longrightarrow> P q"
     1.6        proof (rule+)
     1.7 -	fix q
     1.8 -	assume "Suc (q + k) = m"
     1.9 -	hence "(Suc q) + k = m"
    1.10 -	  by simp
    1.11 -	with ind
    1.12 -	have psq: "P (Suc q)"
    1.13 -	  by simp
    1.14 -	from alln
    1.15 -	have "P (Suc q) --> P q"
    1.16 -	  ..
    1.17 -	with psq
    1.18 -	show "P q"
    1.19 -	  by simp
    1.20 +        fix q
    1.21 +        assume "Suc (q + k) = m"
    1.22 +        hence "(Suc q) + k = m"
    1.23 +          by simp
    1.24 +        with ind
    1.25 +        have psq: "P (Suc q)"
    1.26 +          by simp
    1.27 +        from alln
    1.28 +        have "P (Suc q) --> P q"
    1.29 +          ..
    1.30 +        with psq
    1.31 +        show "P q"
    1.32 +          by simp
    1.33        qed
    1.34      qed
    1.35    qed
    1.36 @@ -457,9 +457,9 @@
    1.37        assume "P x"
    1.38        from allx
    1.39        have "P x \<longrightarrow> 0 < x"
    1.40 -	..
    1.41 +        ..
    1.42        thus "0 < x"
    1.43 -	by (simp add: prems)
    1.44 +        by (simp add: prems)
    1.45      qed
    1.46    next
    1.47      from px