2005-03-25 paulson [Fri, 25 Mar 2005 16:20:57 +0100] rev 15628
tidied up
src/HOL/Library/Primes.thy src/HOL/NumberTheory/Fib.thy

2005-03-25 aspinall [Fri, 25 Mar 2005 14:14:01 +0100] rev 15627
Revert previous change (but leave comments).
src/Pure/General/url.ML

2005-03-25 aspinall [Fri, 25 Mar 2005 14:04:42 +0100] rev 15626
Support new PGIP commands redostep, redoitem
src/Pure/proof_general.ML

2005-03-25 aspinall [Fri, 25 Mar 2005 13:03:47 +0100] rev 15625
Support non-standard file: URL syntax, temporarily.
src/Pure/General/url.ML

2005-03-24 ballarin [Thu, 24 Mar 2005 17:03:37 +0100] rev 15624
Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.
etc/isar-keywords-ZF.el etc/isar-keywords.el src/FOL/ex/LocaleTest.thy src/Pure/General/name_space.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/isar_thy.ML src/Pure/Isar/locale.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/pure_thy.ML src/Pure/sign.ML

2005-03-24 ballarin [Thu, 24 Mar 2005 16:36:40 +0100] rev 15623
*** empty log message ***
src/Pure/Isar/locale.ML

2005-03-24 ballarin [Thu, 24 Mar 2005 16:34:15 +0100] rev 15622
Transitivity reasoner ignores types amenable to linear arithmetic.
These are currently nat, int, real.

Fixed IsaMakefile.
src/HOL/IsaMakefile src/HOL/Orderings.thy

2005-03-24 paulson [Thu, 24 Mar 2005 10:59:21 +0100] rev 15621
COMMENT IN WRONG PLACE
src/HOL/IsaMakefile

2005-03-23 paulson [Wed, 23 Mar 2005 12:09:18 +0100] rev 15620
replaced bool by a new datatype "bit" for binary numerals
src/HOL/Integ/IntDiv.thy src/HOL/Integ/NatBin.thy src/HOL/Integ/Numeral.thy src/HOL/Integ/presburger.ML src/HOL/Library/Word.thy src/HOL/Tools/Presburger/presburger.ML src/HOL/Tools/numeral_syntax.ML src/HOL/hologic.ML

2005-03-23 paulson [Wed, 23 Mar 2005 12:08:52 +0100] rev 15619
temporary removal of Import
src/HOL/IsaMakefile