| changeset 42416 | a8a9f4d79196 |
| parent 41637 | 55a45051b220 |
| child 46950 | d0181abdbdac |
--- a/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 19 12:22:59 2011 +0200 +++ b/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 19 14:17:41 2011 +0200 @@ -69,7 +69,7 @@ text {* Enumeration types *} -class enum = ord + finite + +class spark_enum = ord + finite + fixes pos :: "'a \<Rightarrow> int" assumes range_pos: "range pos = {0..<int (card (UNIV::'a set))}" and less_pos: "(x < y) = (pos x < pos y)"