src/HOL/Lambda/Commutation.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -25,9 +25,9 @@
     1.4    "Church_Rosser R =
     1.5      (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    confluent :: "('a \<times> 'a) set => bool"
    1.10 -  "confluent R = diamond (R^*)"
    1.11 +  "confluent R == diamond (R^*)"
    1.12  
    1.13  
    1.14  subsection {* Basic lemmas *}