src/HOL/Integ/Parity.thy
changeset 17472 bcbf48d59059
parent 17085 5b57f995a179
child 18648 22f96cd085d5
     1.1 --- a/src/HOL/Integ/Parity.thy	Sat Sep 17 18:24:57 2005 +0200
     1.2 +++ b/src/HOL/Integ/Parity.thy	Sat Sep 17 18:25:11 2005 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Jeremy Avigad
     1.5  *)
     1.6  
     1.7 -header {* Parity: Even and Odd for ints and nats*}
     1.8 +header {* Even and Odd for ints and nats*}
     1.9  
    1.10  theory Parity
    1.11  imports Divides IntDiv NatSimprocs
    1.12 @@ -397,7 +397,7 @@
    1.13  declare power_even_abs_number_of [simp]
    1.14  
    1.15  
    1.16 -subsection {* An Equivalence for @{term "0 \<le> a^n"} *}
    1.17 +subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
    1.18  
    1.19  lemma even_power_le_0_imp_0:
    1.20       "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"