--- a/Nominal/Test.thy	Mon Mar 08 16:11:42 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 08 20:18:27 2010 +0100
@@ -70,9 +70,9 @@
 | "f (PD x y) = {atom x, atom y}"
 
 (* compat should be
-compat (PN) pi (PN) \<equiv> TRue
-compat (PS x) pi (PS x') \<equiv> pi o x = x'
-compat (PD p1 p2) pi (PD p1' p2') \<equiv> compat p1 pi p1' \<and> compat p2 pi p2'
+compat (PN) pi (PN) == True
+compat (PS x) pi (PS x') == pi o x = x'
+compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'
 *)
 
 
@@ -160,7 +160,7 @@
   "bv2 (As x t) = {atom x}"
 
 (* compat should be
-compat (As x t) pi (As x' t') \<equiv> pi o x = x' \<and> alpha t t'
+compat (As x t) pi (As x' t') == pi o x = x' & alpha t t'
 *)
 
 
@@ -403,6 +403,13 @@
 where
  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
 
+(*
+compat (K s ts vs) pi (K s' ts' vs') ==
+  s = s' & 
+
+*)
+
+
 (*thm bv_raw.simps*)
 
 (* example 3 from Peter Sewell's bestiary *)