# HG changeset patch # User berghofe # Date 1303215613 -7200 # Node ID 574393cb3d9d9f74ad84a266a907b0ee0012f3e5 # Parent 10accf397ab603e0c14ad1faf2b1c35e0a5e7f3b# Parent a8a9f4d79196f6d55275e868f4eafeb57e5abaa1 merged diff -r 10accf397ab6 -r 574393cb3d9d src/HOL/SPARK/SPARK_Setup.thy --- a/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 19 14:04:58 2011 +0200 +++ b/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 19 14:20:13 2011 +0200 @@ -69,7 +69,7 @@ text {* Enumeration types *} -class enum = ord + finite + +class spark_enum = ord + finite + fixes pos :: "'a \ int" assumes range_pos: "range pos = {0.. - Class.instantiation ([tyname'], [], @{sort enum}) |> + Class.instantiation ([tyname'], [], @{sort spark_enum}) |> define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals (p, @@ -266,7 +266,7 @@ in lthy' |> Local_Theory.note - ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>> + ((Binding.name (tyname ^ "_card"), simp_att), [card_UNIV]) ||>> Local_Theory.note ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>> Local_Theory.note