2004-08-05 paulson [Thu, 05 Aug 2004 10:51:30 +0200] rev 15114
an updated treatment of the simprules
src/HOL/ex/NatSum.thy

2004-08-05 paulson [Thu, 05 Aug 2004 10:50:58 +0200] rev 15113
some structured proofs
src/HOL/List.thy

2004-08-04 nipkow [Wed, 04 Aug 2004 19:12:15 +0200] rev 15112
added a thm
src/HOL/Relation_Power.thy

2004-08-04 nipkow [Wed, 04 Aug 2004 19:11:02 +0200] rev 15111
added some inj_on thms
src/HOL/Finite_Set.thy src/HOL/Fun.thy

2004-08-04 nipkow [Wed, 04 Aug 2004 19:10:45 +0200] rev 15110
Added a number of new thms and the new function remove1
src/HOL/List.thy src/HOL/Map.thy

2004-08-04 nipkow [Wed, 04 Aug 2004 19:09:58 +0200] rev 15109
proof mod
src/HOL/MicroJava/BV/LBVSpec.thy src/HOL/NumberTheory/Finite2.thy

2004-08-04 nipkow [Wed, 04 Aug 2004 19:09:41 +0200] rev 15108
added a few thms
src/HOL/Integ/Equiv.thy

2004-08-04 chaieb [Wed, 04 Aug 2004 17:43:55 +0200] rev 15107
oracle corrected
src/HOL/Integ/cooper_dec.ML src/HOL/Integ/cooper_proof.ML src/HOL/Tools/Presburger/cooper_dec.ML src/HOL/Tools/Presburger/cooper_proof.ML

2004-08-04 nipkow [Wed, 04 Aug 2004 11:25:08 +0200] rev 15106
aded comment
doc-src/TutorialI/CTL/CTL.thy doc-src/TutorialI/CTL/document/CTL.tex

2004-08-04 nipkow [Wed, 04 Aug 2004 09:44:40 +0200] rev 15105
fixed tex problem
src/HOL/Hyperreal/Integration.thy