# HG changeset patch
# User huffman
# Date 1187801634 -7200
# Node ID d96eb21fc1bc3257624ea439da8303ebb1516935
# Parent  30887caeba62fc304fd7bf74b0adcc975d60c9cd
rename type pls to num0

diff -r 30887caeba62 -r d96eb21fc1bc src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Wed Aug 22 17:58:37 2007 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Aug 22 18:53:54 2007 +0200
@@ -79,7 +79,7 @@
 
 subsection {* Numeral Types *}
 
-typedef (open) pls = "UNIV :: nat set" ..
+typedef (open) num0 = "UNIV :: nat set" ..
 typedef (open) num1 = "UNIV :: unit set" ..
 typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" ..
 typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" ..
@@ -117,8 +117,8 @@
   unfolding type_definition.card [OF type_definition_bit1]
   by (simp only: card_prod card_option card_bool)
 
-lemma card_pls: "CARD (pls) = 0"
-  by (simp add: type_definition.card [OF type_definition_pls])
+lemma card_num0: "CARD (num0) = 0"
+  by (simp add: type_definition.card [OF type_definition_num0])
 
 lemmas card_univ_simps [simp] =
   card_unit
@@ -130,7 +130,7 @@
   card_num1
   card_bit0
   card_bit1
-  card_pls
+  card_num0
 
 subsection {* Syntax *}
 
@@ -142,13 +142,13 @@
 
 translations
   "_NumeralType1" == (type) "num1"
-  "_NumeralType0" == (type) "pls"
+  "_NumeralType0" == (type) "num0"
 
 parse_translation {*
 let
 
 val num1_const = Syntax.const "Numeral_Type.num1";
-val pls_const = Syntax.const "Numeral_Type.pls";
+val num0_const = Syntax.const "Numeral_Type.num0";
 val B0_const = Syntax.const "Numeral_Type.bit0";
 val B1_const = Syntax.const "Numeral_Type.bit1";
 
@@ -157,7 +157,7 @@
     fun mk_bit n = if n = 0 then B0_const else B1_const;
     fun bin_of n =
       if n = 1 then num1_const
-      else if n = 0 then pls_const
+      else if n = 0 then num0_const
       else if n = ~1 then raise TERM ("negative type numeral", [])
       else
         let val (q, r) = IntInf.divMod (n, 2);
@@ -176,7 +176,7 @@
 fun int_of [] = 0
   | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
 
-fun bin_of (Const ("pls", _)) = []
+fun bin_of (Const ("num0", _)) = []
   | bin_of (Const ("num1", _)) = [1]
   | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
   | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
diff -r 30887caeba62 -r d96eb21fc1bc src/HOL/Word/Size.thy
--- a/src/HOL/Word/Size.thy	Wed Aug 22 17:58:37 2007 +0200
+++ b/src/HOL/Word/Size.thy	Wed Aug 22 18:53:54 2007 +0200
@@ -25,18 +25,18 @@
 axclass len < len0
   len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
 
-instance pls  :: len0 ..
+instance num0  :: len0 ..
 instance num1 :: len0 ..
 instance bit0 :: (len0) len0 ..
 instance bit1 :: (len0) len0 ..
 
 defs (overloaded)
-  len_pls:  "len_of (x::pls itself) == 0"
+  len_num0: "len_of (x::num0 itself) == 0"
   len_num1: "len_of (x::num1 itself) == 1"
   len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
   len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
 
-lemmas len_of_numeral_defs [simp] = len_pls len_num1 len_bit0 len_bit1
+lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
 
 instance num1 :: len by (intro_classes) simp
 instance bit0 :: (len) len by (intro_classes) simp