1.1 --- a/src/HOL/Nominal/Examples/Class2.thy	Sat Aug 13 22:04:07 2011 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Class2.thy	Sat Aug 13 18:10:14 2011 -0700
     1.3 @@ -3245,7 +3245,7 @@
     1.4    { case 1 show ?case 
     1.5        apply -
     1.6        apply(simp add: lfp_eqvt)
     1.7 -      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     1.8 +      apply(simp add: perm_fun_def [where 'a="ntrm set"])
     1.9        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
    1.10        apply(perm_simp)
    1.11      done
    1.12 @@ -3256,7 +3256,7 @@
    1.13        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
    1.14        apply(simp add: lfp_eqvt)
    1.15        apply(simp add: comp_def)
    1.16 -      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.17 +      apply(simp add: perm_fun_def [where 'a="ntrm set"])
    1.18        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
    1.19        apply(perm_simp)
    1.20        done
    1.21 @@ -3269,7 +3269,7 @@
    1.22      apply -
    1.23      apply(simp only: lfp_eqvt)
    1.24      apply(simp only: comp_def)
    1.25 -    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.26 +    apply(simp only: perm_fun_def [where 'a="ntrm set"])
    1.27      apply(simp only: NEGc.simps NEGn.simps)
    1.28      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
    1.29      apply(perm_simp add: ih1 ih2)
    1.30 @@ -3289,7 +3289,7 @@
    1.31      apply -
    1.32      apply(simp only: lfp_eqvt)
    1.33      apply(simp only: comp_def)
    1.34 -    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.35 +    apply(simp only: perm_fun_def [where 'a="ntrm set"])
    1.36      apply(simp only: NEGc.simps NEGn.simps)
    1.37      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name 
    1.38                       ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
    1.39 @@ -3311,7 +3311,7 @@
    1.40      apply -
    1.41      apply(simp only: lfp_eqvt)
    1.42      apply(simp only: comp_def)
    1.43 -    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.44 +    apply(simp only: perm_fun_def [where 'a="ntrm set"])
    1.45      apply(simp only: NEGc.simps NEGn.simps)
    1.46      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name 
    1.47                       ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
    1.48 @@ -3333,7 +3333,7 @@
    1.49      apply -
    1.50      apply(simp only: lfp_eqvt)
    1.51      apply(simp only: comp_def)
    1.52 -    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.53 +    apply(simp only: perm_fun_def [where 'a="ntrm set"])
    1.54      apply(simp only: NEGc.simps NEGn.simps)
    1.55      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
    1.56      apply(perm_simp add: ih1 ih2 ih3 ih4)
    1.57 @@ -3355,7 +3355,7 @@
    1.58    { case 1 show ?case 
    1.59        apply -
    1.60        apply(simp add: lfp_eqvt)
    1.61 -      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.62 +      apply(simp add: perm_fun_def [where 'a="ntrm set"])
    1.63        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
    1.64        apply(perm_simp)
    1.65      done
    1.66 @@ -3366,7 +3366,7 @@
    1.67        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
    1.68        apply(simp add: lfp_eqvt)
    1.69        apply(simp add: comp_def)
    1.70 -      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.71 +      apply(simp add: perm_fun_def [where 'a="ntrm set"])
    1.72        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
    1.73        apply(perm_simp)
    1.74        done
    1.75 @@ -3379,7 +3379,7 @@
    1.76      apply -
    1.77      apply(simp only: lfp_eqvt)
    1.78      apply(simp only: comp_def)
    1.79 -    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.80 +    apply(simp only: perm_fun_def [where 'a="ntrm set"])
    1.81      apply(simp only: NEGc.simps NEGn.simps)
    1.82      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
    1.83              NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
    1.84 @@ -3401,7 +3401,7 @@
    1.85      apply -
    1.86      apply(simp only: lfp_eqvt)
    1.87      apply(simp only: comp_def)
    1.88 -    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.89 +    apply(simp only: perm_fun_def [where 'a="ntrm set"])
    1.90      apply(simp only: NEGc.simps NEGn.simps)
    1.91      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname 
    1.92                       ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
    1.93 @@ -3423,7 +3423,7 @@
    1.94      apply -
    1.95      apply(simp only: lfp_eqvt)
    1.96      apply(simp only: comp_def)
    1.97 -    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
    1.98 +    apply(simp only: perm_fun_def [where 'a="ntrm set"])
    1.99      apply(simp only: NEGc.simps NEGn.simps)
   1.100      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname 
   1.101                       ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
   1.102 @@ -3445,7 +3445,7 @@
   1.103      apply -
   1.104      apply(simp only: lfp_eqvt)
   1.105      apply(simp only: comp_def)
   1.106 -    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
   1.107 +    apply(simp only: perm_fun_def [where 'a="ntrm set"])
   1.108      apply(simp only: NEGc.simps NEGn.simps)
   1.109      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname 
   1.110           IMPLEFT_eqvt_coname)