src/HOL/Library/Accessible_Part.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
     1.1 --- a/src/HOL/Library/Accessible_Part.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Library/Accessible_Part.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    intros
     1.5      accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    termi :: "('a \<times> 'a) set => 'a set"
    1.10    "termi r == acc (r\<inverse>)"
    1.11