src/HOL/Word/Size.thy
changeset 24406 d96eb21fc1bc
parent 24333 e77ea0ea7f2c
     1.1 --- a/src/HOL/Word/Size.thy	Wed Aug 22 17:58:37 2007 +0200
     1.2 +++ b/src/HOL/Word/Size.thy	Wed Aug 22 18:53:54 2007 +0200
     1.3 @@ -25,18 +25,18 @@
     1.4  axclass len < len0
     1.5    len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
     1.6  
     1.7 -instance pls  :: len0 ..
     1.8 +instance num0  :: len0 ..
     1.9  instance num1 :: len0 ..
    1.10  instance bit0 :: (len0) len0 ..
    1.11  instance bit1 :: (len0) len0 ..
    1.12  
    1.13  defs (overloaded)
    1.14 -  len_pls:  "len_of (x::pls itself) == 0"
    1.15 +  len_num0: "len_of (x::num0 itself) == 0"
    1.16    len_num1: "len_of (x::num1 itself) == 1"
    1.17    len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
    1.18    len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
    1.19  
    1.20 -lemmas len_of_numeral_defs [simp] = len_pls len_num1 len_bit0 len_bit1
    1.21 +lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    1.22  
    1.23  instance num1 :: len by (intro_classes) simp
    1.24  instance bit0 :: (len) len by (intro_classes) simp