2001-01-05 paulson [Fri, 05 Jan 2001 10:19:14 +0100] rev 10786
Field of a relation, and some Domain/Range rules
src/HOL/Relation.ML src/HOL/Relation.thy

2001-01-05 paulson [Fri, 05 Jan 2001 10:18:46 +0100] rev 10785
finite_trancl: new theorem by Sidi Ehmety
src/HOL/Finite.ML

2001-01-05 paulson [Fri, 05 Jan 2001 10:17:48 +0100] rev 10784
more removal of obsolete rules
src/HOL/Hyperreal/HRealAbs.ML src/HOL/Hyperreal/HyperArith0.ML src/HOL/Hyperreal/HyperBin.ML src/HOL/Hyperreal/HyperNat.ML src/HOL/Hyperreal/HyperOrd.ML src/HOL/Hyperreal/HyperPow.ML src/HOL/Hyperreal/SEQ.ML src/HOL/Hyperreal/Series.ML src/HOL/Hyperreal/hypreal_arith0.ML src/HOL/Real/RComplete.ML src/HOL/Real/RealArith0.ML src/HOL/Real/RealBin.ML src/HOL/Real/RealInt.ML src/HOL/Real/RealOrd.ML src/HOL/Real/RealPow.ML

2001-01-05 paulson [Fri, 05 Jan 2001 10:17:19 +0100] rev 10783
fixed two proofs that were affected by the removal of obsolete rules
src/HOL/Real/HahnBanach/Aux.thy

2001-01-05 paulson [Fri, 05 Jan 2001 10:15:48 +0100] rev 10782
new examples by Sidi Ehmety
src/HOL/UNITY/Counter.ML src/HOL/UNITY/Counter.thy src/HOL/UNITY/Counterc.ML src/HOL/UNITY/Counterc.thy src/HOL/UNITY/Priority.ML src/HOL/UNITY/Priority.thy src/HOL/UNITY/PriorityAux.ML src/HOL/UNITY/PriorityAux.thy src/HOL/UNITY/ROOT.ML

2001-01-04 wenzelm [Thu, 04 Jan 2001 19:41:13 +0100] rev 10781
tuned comment;
TFL/rules.ML

2001-01-04 wenzelm [Thu, 04 Jan 2001 19:39:53 +0100] rev 10780
renamed .sml files to .ML;
TFL/dcterm.sml TFL/post.sml TFL/rules.sml TFL/tfl.sml TFL/thms.sml TFL/thry.sml TFL/usyntax.sml TFL/utils.sml

2001-01-04 nipkow [Thu, 04 Jan 2001 18:13:27 +0100] rev 10779
label!
doc-src/TutorialI/Types/numerics.tex

2001-01-04 paulson [Thu, 04 Jan 2001 10:23:01 +0100] rev 10778
more tidying, especially to remove real_of_posnat
src/HOL/Hyperreal/HRealAbs.ML src/HOL/Hyperreal/HRealAbs.thy src/HOL/Hyperreal/HSeries.ML src/HOL/Hyperreal/HyperBin.ML src/HOL/Hyperreal/HyperDef.ML src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/HyperNat.ML src/HOL/Hyperreal/HyperNat.thy src/HOL/Hyperreal/HyperOrd.ML src/HOL/Hyperreal/HyperPow.ML src/HOL/Hyperreal/HyperPow.thy src/HOL/Hyperreal/Lim.ML src/HOL/Hyperreal/NSA.ML src/HOL/Hyperreal/NatStar.ML src/HOL/Hyperreal/NatStar.thy src/HOL/Hyperreal/SEQ.ML src/HOL/Hyperreal/Series.ML src/HOL/Hyperreal/Star.ML src/HOL/Real/RComplete.ML src/HOL/Real/RealArith0.ML src/HOL/Real/RealDef.thy src/HOL/Real/RealOrd.ML src/HOL/Real/RealPow.ML

2001-01-04 paulson [Thu, 04 Jan 2001 10:22:33 +0100] rev 10777
initial material on the Reals
doc-src/TutorialI/Types/Numbers.thy doc-src/TutorialI/Types/document/Typedef.tex doc-src/TutorialI/Types/numerics.tex