changeset 21404 | eb85850d3eb7 |
parent 19669 | 95ac857276e1 |
child 22262 | 96ba62dff413 |
--- a/src/HOL/Accessible_Part.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Accessible_Part.thy Fri Nov 17 02:20:03 2006 +0100 @@ -24,7 +24,7 @@ accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r" abbreviation - termi :: "('a \<times> 'a) set => 'a set" + termi :: "('a \<times> 'a) set => 'a set" where "termi r == acc (r\<inverse>)"