--- a/src/HOL/Datatype_Universe.thy Sat Sep 17 18:24:57 2005 +0200
+++ b/src/HOL/Datatype_Universe.thy Sat Sep 17 18:25:11 2005 +0200
@@ -145,7 +145,7 @@
done
-subsubsection{*Freeness: Distinctness of Constructors*}
+subsection{*Freeness: Distinctness of Constructors*}
(** Scons vs Atom **)
--- a/src/HOL/Integ/IntArith.thy Sat Sep 17 18:24:57 2005 +0200
+++ b/src/HOL/Integ/IntArith.thy Sat Sep 17 18:25:11 2005 +0200
@@ -226,7 +226,7 @@
done
-subsubsection "Induction principles for int"
+subsection "Induction principles for int"
(* `set:int': dummy construction *)
theorem int_ge_induct[case_names base step,induct set:int]:
--- a/src/HOL/Integ/NatSimprocs.thy Sat Sep 17 18:24:57 2005 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy Sat Sep 17 18:25:11 2005 +0200
@@ -346,7 +346,7 @@
divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
-subsubsection{*Division By @{term "-1"}*}
+subsubsection{*Division By @{text "-1"}*}
lemma divide_minus1 [simp]:
"x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
--- a/src/HOL/Integ/Parity.thy Sat Sep 17 18:24:57 2005 +0200
+++ b/src/HOL/Integ/Parity.thy Sat Sep 17 18:25:11 2005 +0200
@@ -3,7 +3,7 @@
Author: Jeremy Avigad
*)
-header {* Parity: Even and Odd for ints and nats*}
+header {* Even and Odd for ints and nats*}
theory Parity
imports Divides IntDiv NatSimprocs
@@ -397,7 +397,7 @@
declare power_even_abs_number_of [simp]
-subsection {* An Equivalence for @{term "0 \<le> a^n"} *}
+subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
lemma even_power_le_0_imp_0:
"a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"