src/HOL/Lambda/Commutation.thy

--- a/src/HOL/Lambda/Commutation.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -25,9 +25,9 @@
   "Church_Rosser R =
     (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
 
-abbreviation (output)
+abbreviation
   confluent :: "('a \<times> 'a) set => bool"
-  "confluent R = diamond (R^*)"
+  "confluent R == diamond (R^*)"
 
 
 subsection {* Basic lemmas *}