src/HOL/SEQ.thy
changeset 35216 7641e8d831d2
parent 33271 7be66dee1a5a
child 35292 e4a431b6d9b7
     1.1 --- a/src/HOL/SEQ.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/SEQ.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -573,7 +573,7 @@
     1.4  apply (rule allI, rule impI, rule ext)
     1.5  apply (erule conjE)
     1.6  apply (induct_tac x)
     1.7 -apply (simp add: nat_rec_0)
     1.8 +apply simp
     1.9  apply (erule_tac x="n" in allE)
    1.10  apply (simp)
    1.11  done