2005-06-11 wenzelm [Sat, 11 Jun 2005 22:15:48 +0200] rev 16364
refer to name spaces values instead of names;
src/HOL/Tools/datatype_package.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/record_package.ML src/HOLCF/holcf_logic.ML src/Pure/axclass.ML src/Pure/codegen.ML src/Pure/display.ML src/ZF/Tools/induct_tacs.ML

2005-06-11 wenzelm [Sat, 11 Jun 2005 22:15:47 +0200] rev 16363
renamed Sign.intern_tycon to Sign.intern_type;
src/HOL/Import/proof_kernel.ML src/Pure/Proof/extraction.ML

2005-06-11 wenzelm [Sat, 11 Jun 2005 15:42:51 +0200] rev 16362
fixed spelling;
Admin/isatest-check

2005-06-11 obua [Sat, 11 Jun 2005 12:55:25 +0200] rev 16361
further optimizations of cycle test
src/Pure/defs.ML

2005-06-10 nipkow [Fri, 10 Jun 2005 19:21:16 +0200] rev 16360
tuned
doc-src/TutorialI/ToyList/ToyList.thy

2005-06-10 nipkow [Fri, 10 Jun 2005 18:36:47 +0200] rev 16359
tuning
doc-src/TutorialI/Misc/document/simp.tex doc-src/TutorialI/Misc/simp.thy doc-src/TutorialI/Rules/rules.tex doc-src/TutorialI/Types/numerics.tex doc-src/TutorialI/basics.tex doc-src/TutorialI/tutorial.tex

2005-06-10 nipkow [Fri, 10 Jun 2005 17:59:12 +0200] rev 16358
IntInf change
src/HOL/arith_data.ML src/Provers/Arith/fast_lin_arith.ML

2005-06-10 quigley [Fri, 10 Jun 2005 16:15:36 +0200] rev 16357
All subgoals sent to the watcher at once now.
Rules added to parser for Spass proofs.
If parsing or translation fails on a proof, the Spass proof is printed out in PG.
src/HOL/Tools/ATP/SpassCommunication.ML src/HOL/Tools/ATP/recon_parse.ML src/HOL/Tools/ATP/recon_transfer_proof.ML src/HOL/Tools/ATP/recon_translate_proof.ML src/HOL/Tools/ATP/res_clasimpset.ML src/HOL/Tools/ATP/watcher.ML src/HOL/Tools/res_atp.ML

2005-06-09 wenzelm [Thu, 09 Jun 2005 23:33:28 +0200] rev 16356
added Isar_examples/Drinker.thy;
src/HOL/IsaMakefile src/HOL/Isar_examples/Drinker.thy src/HOL/Isar_examples/ROOT.ML

2005-06-09 wenzelm [Thu, 09 Jun 2005 16:58:03 +0200] rev 16355
full Display.pprint_theory for ML toplevel facilitates debugging;
src/Pure/install_pp.ML