diff -r fa31452b9af6 -r bcbf48d59059 src/HOL/Integ/Parity.thy
--- 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"