# HG changeset patch
# User huffman
# Date 1325055497 -3600
# Node ID ebbc2d5cd72065432f61cf0d376234ee2e53c139
# Parent  5cb7ef5bfef21b15ce36c2ff23ce1642ab838a27
add section headings

diff -r 5cb7ef5bfef2 -r ebbc2d5cd720 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Dec 27 18:26:15 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 28 07:58:17 2011 +0100
@@ -456,6 +456,8 @@
 (* FIXME: only provide one theorem name *)
 lemmas of_nth_def = word_set_bits_def
 
+subsection {* Theorems about typedefs *}
+
 lemma sint_sbintrunc': 
   "sint (word_of_int bin :: 'a word) = 
     (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
@@ -664,6 +666,8 @@
   "x \<le> - (2 ^ (size (w::'a::len word) - 1)) \<Longrightarrow> x \<le> sint w"
   unfolding word_size by (rule order_trans [OF _ sint_ge])
 
+subsection {* Testing bits *}
+
 lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
   unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
 
@@ -4135,7 +4139,7 @@
 declare word_roti_def [simp]
 
 
-subsection {* Miscellaneous  *}
+subsection {* Maximum machine word *}
 
 lemma word_int_cases:
   "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
@@ -4454,6 +4458,8 @@
   apply (case_tac "1+n = 0", auto)
   done
 
+subsection {* Recursion combinator for words *}
+
 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
   "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"