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
```