| changeset 41818 | 6d4c3ee8219d |
| parent 31795 | be3e1cc5005c |
| child 44887 | 7ca82df6e951 |
--- a/src/HOL/Hahn_Banach/Function_Order.thy Tue Feb 22 16:47:18 2011 +0100 +++ b/src/HOL/Hahn_Banach/Function_Order.thy Tue Feb 22 17:06:14 2011 +0100 @@ -21,7 +21,7 @@ graph. *} -types 'a graph = "('a \<times> real) set" +type_synonym 'a graph = "('a \<times> real) set" definition graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where