2007-10-06 wenzelm [Sat, 06 Oct 2007 16:50:04 +0200] rev 24867
simplified interfaces for outer syntax;
NEWS src/HOL/Import/import_syntax.ML src/HOL/Library/Eval.thy src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_package.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Orderings.thy src/HOL/Tools/datatype_package.ML src/HOL/Tools/function_package/fundef_datatype.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/inductive_set_package.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/record_package.ML src/HOL/Tools/refute_isar.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/specification_package.ML src/HOL/Tools/typedef_package.ML src/HOLCF/IOA/meta_theory/ioa_package.ML src/HOLCF/Tools/cont_consts.ML src/HOLCF/Tools/domain/domain_extender.ML src/HOLCF/Tools/fixrec_package.ML src/HOLCF/Tools/pcpodef_package.ML src/Provers/classical.ML src/Pure/Proof/extraction.ML src/Pure/ProofGeneral/proof_general_emacs.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/Tools/invoke.ML src/Pure/Tools/named_thms.ML src/Pure/codegen.ML src/Tools/code/code_package.ML src/Tools/code/code_target.ML src/Tools/induct.ML src/Tools/nbe.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/ind_cases.ML src/ZF/Tools/induct_tacs.ML src/ZF/Tools/inductive_package.ML src/ZF/Tools/primrec_package.ML src/ZF/Tools/typechk.ML

2007-10-06 wenzelm [Sat, 06 Oct 2007 16:41:22 +0200] rev 24866
updated;
etc/isar-keywords-HOL-Nominal.el etc/isar-keywords-ZF.el etc/isar-keywords.el

2007-10-05 wenzelm [Fri, 05 Oct 2007 23:04:17 +0200] rev 24865
(co)induct: polymorhic taking'';
src/Tools/induct.ML

2007-10-05 wenzelm [Fri, 05 Oct 2007 23:04:16 +0200] rev 24864
added burrow_options;
src/Pure/library.ML

2007-10-05 wenzelm [Fri, 05 Oct 2007 23:04:14 +0200] rev 24863
tuned proofs (via polymorphic taking'');
src/HOL/Library/Coinductive_List.thy

2007-10-05 wenzelm [Fri, 05 Oct 2007 22:00:17 +0200] rev 24862
export get_consumes;
src/Pure/Isar/rule_cases.ML

2007-10-05 wenzelm [Fri, 05 Oct 2007 22:00:15 +0200] rev 24861
tuned Induct interface: prefer pred'' over set'';
src/HOL/Nominal/nominal_inductive.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/typedef_package.ML src/Tools/induct.ML src/ZF/Tools/inductive_package.ML

2007-10-05 wenzelm [Fri, 05 Oct 2007 22:00:13 +0200] rev 24860
coinduct: instantiation refers to suffix of main prop (major premise or conclusion);
tuned;
src/HOL/Library/Coinductive_List.thy

2007-10-05 wenzelm [Fri, 05 Oct 2007 22:00:11 +0200] rev 24859
tuned induct etc.;
NEWS doc-src/IsarRef/generic.tex

2007-10-05 wenzelm [Fri, 05 Oct 2007 20:10:35 +0200] rev 24858
execute/system: non-critical;
src/Pure/General/secure.ML