src/HOL/Datatype.thy
changeset 55417 01fbfb60c33e
parent 55415 05f5fdb8d093
child 55642 63beb38e9258
     1.1 --- a/src/HOL/Datatype.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Wed Feb 12 08:37:06 2014 +0100
     1.3 @@ -133,7 +133,7 @@
     1.4  
     1.5  lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
     1.6  apply (simp add: Node_def Push_def) 
     1.7 -apply (fast intro!: apfst_conv case_nat_Suc [THEN trans])
     1.8 +apply (fast intro!: apfst_conv nat.cases(2)[THEN trans])
     1.9  done
    1.10  
    1.11