tuned document;
authorwenzelm
Sat Sep 17 18:25:11 2005 +0200 (2005-09-17)
changeset 17472bcbf48d59059
parent 17471 fa31452b9af6
child 17473 e62a16c5ad82
tuned document;
src/HOL/Datatype_Universe.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/NatSimprocs.thy
src/HOL/Integ/Parity.thy
     1.1 --- a/src/HOL/Datatype_Universe.thy	Sat Sep 17 18:24:57 2005 +0200
     1.2 +++ b/src/HOL/Datatype_Universe.thy	Sat Sep 17 18:25:11 2005 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4  done
     1.5  
     1.6  
     1.7 -subsubsection{*Freeness: Distinctness of Constructors*}
     1.8 +subsection{*Freeness: Distinctness of Constructors*}
     1.9  
    1.10  (** Scons vs Atom **)
    1.11  
     2.1 --- a/src/HOL/Integ/IntArith.thy	Sat Sep 17 18:24:57 2005 +0200
     2.2 +++ b/src/HOL/Integ/IntArith.thy	Sat Sep 17 18:25:11 2005 +0200
     2.3 @@ -226,7 +226,7 @@
     2.4  done
     2.5  
     2.6  
     2.7 -subsubsection "Induction principles for int"
     2.8 +subsection "Induction principles for int"
     2.9  
    2.10                       (* `set:int': dummy construction *)
    2.11  theorem int_ge_induct[case_names base step,induct set:int]:
     3.1 --- a/src/HOL/Integ/NatSimprocs.thy	Sat Sep 17 18:24:57 2005 +0200
     3.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Sat Sep 17 18:25:11 2005 +0200
     3.3 @@ -346,7 +346,7 @@
     3.4    divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
     3.5    le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
     3.6  
     3.7 -subsubsection{*Division By @{term "-1"}*}
     3.8 +subsubsection{*Division By @{text "-1"}*}
     3.9  
    3.10  lemma divide_minus1 [simp]:
    3.11       "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" 
     4.1 --- a/src/HOL/Integ/Parity.thy	Sat Sep 17 18:24:57 2005 +0200
     4.2 +++ b/src/HOL/Integ/Parity.thy	Sat Sep 17 18:25:11 2005 +0200
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     Jeremy Avigad
     4.5  *)
     4.6  
     4.7 -header {* Parity: Even and Odd for ints and nats*}
     4.8 +header {* Even and Odd for ints and nats*}
     4.9  
    4.10  theory Parity
    4.11  imports Divides IntDiv NatSimprocs
    4.12 @@ -397,7 +397,7 @@
    4.13  declare power_even_abs_number_of [simp]
    4.14  
    4.15  
    4.16 -subsection {* An Equivalence for @{term "0 \<le> a^n"} *}
    4.17 +subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
    4.18  
    4.19  lemma even_power_le_0_imp_0:
    4.20       "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"