# HG changeset patch
# User huffman
# Date 1313284214 25200
# Node ID 013f7b14f6ff343e814e27e1f0af4769b6a95dd1
# Parent  a32ca91659281777e3e427c66f9c1cb9e4a3ae35
HOL-Nominal-Examples: respect distinction between sets and functions

diff -r a32ca9165928 -r 013f7b14f6ff src/HOL/Nominal/Examples/Class2.thy
--- a/src/HOL/Nominal/Examples/Class2.thy	Sat Aug 13 22:04:07 2011 +0200
+++ b/src/HOL/Nominal/Examples/Class2.thy	Sat Aug 13 18:10:14 2011 -0700
@@ -3245,7 +3245,7 @@
   { case 1 show ?case 
       apply -
       apply(simp add: lfp_eqvt)
-      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+      apply(simp add: perm_fun_def [where 'a="ntrm set"])
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(perm_simp)
     done
@@ -3256,7 +3256,7 @@
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(simp add: lfp_eqvt)
       apply(simp add: comp_def)
-      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+      apply(simp add: perm_fun_def [where 'a="ntrm set"])
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(perm_simp)
       done
@@ -3269,7 +3269,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
     apply(perm_simp add: ih1 ih2)
@@ -3289,7 +3289,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name 
                      ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
@@ -3311,7 +3311,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name 
                      ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
@@ -3333,7 +3333,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
     apply(perm_simp add: ih1 ih2 ih3 ih4)
@@ -3355,7 +3355,7 @@
   { case 1 show ?case 
       apply -
       apply(simp add: lfp_eqvt)
-      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+      apply(simp add: perm_fun_def [where 'a="ntrm set"])
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(perm_simp)
     done
@@ -3366,7 +3366,7 @@
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(simp add: lfp_eqvt)
       apply(simp add: comp_def)
-      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+      apply(simp add: perm_fun_def [where 'a="ntrm set"])
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(perm_simp)
       done
@@ -3379,7 +3379,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
             NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
@@ -3401,7 +3401,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname 
                      ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
@@ -3423,7 +3423,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname 
                      ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
@@ -3445,7 +3445,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
+    apply(simp only: perm_fun_def [where 'a="ntrm set"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname 
          IMPLEFT_eqvt_coname)