2003-05-05 paulson [Mon, 05 May 2003 18:34:16 +0200] rev 13960
Complex, etc
NEWS

2003-05-05 paulson [Mon, 05 May 2003 18:30:48 +0200] rev 13959
deleted obsolete group formalization
src/HOL/GroupTheory/Group.thy src/HOL/GroupTheory/README.html src/HOL/GroupTheory/ROOT.ML src/HOL/GroupTheory/document/root.tex

2003-05-05 paulson [Mon, 05 May 2003 18:23:40 +0200] rev 13958
New material on integration, etc. Moving Hyperreal/ex
to directory Complex
src/HOL/Hyperreal/HLog.ML src/HOL/Hyperreal/HLog.thy src/HOL/Hyperreal/HTranscendental.ML src/HOL/Hyperreal/HTranscendental.thy src/HOL/Hyperreal/Hyperreal.thy src/HOL/Hyperreal/IntFloor.ML src/HOL/Hyperreal/IntFloor.thy src/HOL/Hyperreal/Integration.ML src/HOL/Hyperreal/Integration.thy src/HOL/Hyperreal/ROOT.ML src/HOL/Hyperreal/Transcendental.ML src/HOL/Hyperreal/Transcendental.thy src/HOL/Hyperreal/ex/ROOT.ML src/HOL/Hyperreal/ex/Sqrt.thy src/HOL/Hyperreal/ex/Sqrt_Script.thy src/HOL/Hyperreal/ex/document/root.tex

2003-05-05 paulson [Mon, 05 May 2003 18:22:31 +0200] rev 13957
new session Complex for the complex numbers
src/HOL/Complex/CLim.ML src/HOL/Complex/CLim.thy src/HOL/Complex/CSeries.ML src/HOL/Complex/CSeries.thy src/HOL/Complex/CStar.ML src/HOL/Complex/CStar.thy src/HOL/Complex/Complex.ML src/HOL/Complex/Complex.thy src/HOL/Complex/ComplexArith0.ML src/HOL/Complex/ComplexArith0.thy src/HOL/Complex/ComplexBin.ML src/HOL/Complex/ComplexBin.thy src/HOL/Complex/NSCA.ML src/HOL/Complex/NSCA.thy src/HOL/Complex/NSComplex.ML src/HOL/Complex/NSComplex.thy src/HOL/Complex/NSComplexArith0.ML src/HOL/Complex/NSComplexArith0.thy src/HOL/Complex/NSComplexBin.ML src/HOL/Complex/NSComplexBin.thy src/HOL/Complex/NSInduct.ML src/HOL/Complex/NSInduct.thy src/HOL/Complex/ROOT.ML src/HOL/Complex/ex/NSPrimes.ML src/HOL/Complex/ex/NSPrimes.thy src/HOL/Complex/ex/ROOT.ML src/HOL/Complex/ex/Sqrt.thy src/HOL/Complex/ex/Sqrt_Script.thy src/HOL/Complex/ex/document/root.tex

2003-05-05 paulson [Mon, 05 May 2003 18:22:01 +0200] rev 13956
improved presentation of HOL/Auth theories
src/HOL/Auth/CertifiedEmail.thy src/HOL/Auth/Event.thy src/HOL/Auth/Message.thy src/HOL/Auth/NS_Public.thy src/HOL/Auth/NS_Public_Bad.thy src/HOL/Auth/NS_Shared.thy src/HOL/Auth/Public.thy src/HOL/Auth/Recur.thy src/HOL/Auth/Shared.thy src/HOL/Auth/TLS.thy src/HOL/Auth/Yahalom.thy src/HOL/Auth/Yahalom2.thy src/HOL/Auth/Yahalom_Bad.thy src/HOL/Auth/document/root.tex

2003-05-05 kleing [Mon, 05 May 2003 15:55:56 +0200] rev 13955
add mac test
Admin/isatest-makedist

2003-05-05 kleing [Mon, 05 May 2003 13:52:19 +0200] rev 13954
fixed \<0>..\<9> (-> \<zero>..\<nine>)
NEWS

2003-05-05 kleing [Mon, 05 May 2003 13:42:16 +0200] rev 13953
document preparation tuning
NEWS

2003-05-05 ballarin [Mon, 05 May 2003 10:53:27 +0200] rev 13952
Fixed but with old versions of pdflatex (fancy symbols not allowed in bookmarks).
src/HOL/Algebra/Module.thy

2003-05-03 kleing [Sat, 03 May 2003 13:31:07 +0200] rev 13951
fix for new \isasymeuro
doc-src/System/system.tex