src/HOL/Nominal/Examples/Pattern.thy
changeset 60580 7e741e22d7fc
parent 58889 5b7a9633cfa8
child 61069 aefe89038dd2
     1.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Thu Jun 25 22:56:33 2015 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Thu Jun 25 23:33:47 2015 +0200
     1.3 @@ -62,20 +62,20 @@
     1.4    by (simp add: supp_def Collect_disj_eq del: disj_not1)
     1.5  
     1.6  instance pat :: pt_name
     1.7 -proof intro_classes
     1.8 -  case goal1
     1.9 +proof (default, goals)
    1.10 +  case (1 x)
    1.11    show ?case by (induct x) simp_all
    1.12  next
    1.13 -  case goal2
    1.14 +  case (2 _ _ x)
    1.15    show ?case by (induct x) (simp_all add: pt_name2)
    1.16  next
    1.17 -  case goal3
    1.18 +  case (3 _ _ x)
    1.19    then show ?case by (induct x) (simp_all add: pt_name3)
    1.20  qed
    1.21  
    1.22  instance pat :: fs_name
    1.23 -proof intro_classes
    1.24 -  case goal1
    1.25 +proof (default, goals)
    1.26 +  case (1 x)
    1.27    show ?case by (induct x) (simp_all add: fin_supp)
    1.28  qed
    1.29