# HG changeset patch
# User kleing
# Date 1316139043 -36000
# Node ID 5930d35c976d19558b51f3fdc46ef383699a45c2
# Parent  98e05fc1ce7dacea7b3228537557b11ab25f2454
removed unused legacy lemma names, some comment cleanup.

diff -r 98e05fc1ce7d -r 5930d35c976d src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Fri Sep 16 12:10:15 2011 +1000
+++ b/src/HOL/Word/Bit_Int.thy	Fri Sep 16 12:10:43 2011 +1000
@@ -1,9 +1,9 @@
 (* 
   Author: Jeremy Dawson and Gerwin Klein, NICTA
 
-  definition and basic theorems for bit-wise logical operations 
+  Definitions and basic theorems for bit-wise logical operations 
   for integers expressed using Pls, Min, BIT,
-  and converting them to and from lists of bools
+  and converting them to and from lists of bools.
 *) 
 
 header {* Bitwise Operations on Binary Integers *}
diff -r 98e05fc1ce7d -r 5930d35c976d src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Fri Sep 16 12:10:15 2011 +1000
+++ b/src/HOL/Word/Bit_Representation.thy	Fri Sep 16 12:10:43 2011 +1000
@@ -1,8 +1,7 @@
 (* 
   Author: Jeremy Dawson, NICTA
 
-  contains basic definition to do with integers
-  expressed using Pls, Min, BIT
+  Basic definitions to do with integers, expressed using Pls, Min, BIT.
 *) 
 
 header {* Basic Definitions for Binary Integers *}
@@ -876,8 +875,7 @@
     size list = number_of k"
   by (auto simp: pred_def succ_def split add : split_if_asm)
 
-lemmas ls_splits = 
-  prod.split split_split prod.split_asm split_split_asm split_if_asm
+lemmas ls_splits = prod.split prod.split_asm split_if_asm
 
 lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"
   by (cases y) auto
diff -r 98e05fc1ce7d -r 5930d35c976d src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Sep 16 12:10:15 2011 +1000
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Sep 16 12:10:43 2011 +1000
@@ -1,7 +1,7 @@
 (* 
   Author: Jeremy Dawson, NICTA
 
-  contains theorems to do with integers, expressed using Pls, Min, BIT,
+  Theorems to do with integers, expressed using Pls, Min, BIT,
   theorems linking them to lists of booleans, and repeated splitting 
   and concatenation.
 *) 
@@ -60,8 +60,10 @@
 
 subsection "Arithmetic in terms of bool lists"
 
-(* arithmetic operations in terms of the reversed bool list,
-  assuming input list(s) the same length, and don't extend them *)
+text {* 
+  Arithmetic operations in terms of the reversed bool list,
+  assuming input list(s) the same length, and don't extend them. 
+*}
 
 primrec rbl_succ :: "bool list => bool list" where
   Nil: "rbl_succ Nil = Nil"
@@ -72,13 +74,13 @@
   | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
 
 primrec rbl_add :: "bool list => bool list => bool list" where
-    (* result is length of first arg, second arg may be longer *)
+  -- "result is length of first arg, second arg may be longer"
   Nil: "rbl_add Nil x = Nil"
   | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
     (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
 
 primrec rbl_mult :: "bool list => bool list => bool list" where
-    (* result is length of first arg, second arg may be longer *)
+  -- "result is length of first arg, second arg may be longer"
   Nil: "rbl_mult Nil x = Nil"
   | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
     if y then rbl_add ws x else ws)"
@@ -112,7 +114,7 @@
     bin_to_bl_aux (n - 1) w (True # bl)"
   by (cases n) auto
 
-(** link between bin and bool list **)
+text {* Link between bin and bool list. *}
 
 lemma bl_to_bin_aux_append: 
   "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
diff -r 98e05fc1ce7d -r 5930d35c976d src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Fri Sep 16 12:10:15 2011 +1000
+++ b/src/HOL/Word/Misc_Numeric.thy	Fri Sep 16 12:10:43 2011 +1000
@@ -11,13 +11,6 @@
 lemma the_elemI: "y = {x} ==> the_elem y = x" 
   by simp
 
-lemmas split_split = prod.split
-lemmas split_split_asm = prod.split_asm
-lemmas split_splits = split_split split_split_asm
-
-lemmas funpow_0 = funpow.simps(1)
-lemmas funpow_Suc = funpow.simps(2)
-
 lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto
 
 lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by arith 
diff -r 98e05fc1ce7d -r 5930d35c976d src/HOL/Word/Misc_Typedef.thy
--- a/src/HOL/Word/Misc_Typedef.thy	Fri Sep 16 12:10:15 2011 +1000
+++ b/src/HOL/Word/Misc_Typedef.thy	Fri Sep 16 12:10:43 2011 +1000
@@ -1,8 +1,7 @@
 (* 
-    Author:     Jeremy Dawson and Gerwin Klein, NICTA
+  Author:     Jeremy Dawson and Gerwin Klein, NICTA
 
-  consequences of type definition theorems, 
-  and of extended type definition theorems
+  Consequences of type definition theorems, and of extended type definition. theorems
 *)
 
 header {* Type Definition Theorems *}