2008-06-25 wenzelm [Wed, 25 Jun 2008 17:38:32 +0200] rev 27353
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
doc-src/antiquote_setup.ML src/HOL/Import/import_syntax.ML src/HOL/Import/proof_kernel.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/typedef_package.ML src/HOLCF/IOA/meta_theory/ioa_package.ML src/HOLCF/Tools/domain/domain_extender.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/outer_syntax.ML src/Pure/ProofGeneral/pgip_parser.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/Thy/thy_edit.ML src/Pure/codegen.ML src/Tools/code/code_target.ML src/ZF/Tools/induct_tacs.ML

2008-06-25 berghofe [Wed, 25 Jun 2008 14:54:45 +0200] rev 27352
- Equivariance simpset used in proofs of strong induction and inversion
rules now contains perm_simproc_app and perm_simproc_fun as well
- first_order_matchs now eta-contracts terms before matching
- Rewrote code for proving strong inversion rule to avoid failure when
one of the arguments of the inductive predicate has an atom type
src/HOL/Nominal/nominal_inductive.ML

2008-06-25 wenzelm [Wed, 25 Jun 2008 12:15:05 +0200] rev 27351
pprint: back to proper output of markup, with workaround for Poly/ML crash;
src/Pure/General/pretty.ML

2008-06-24 wenzelm [Tue, 24 Jun 2008 23:38:44 +0200] rev 27350
back to 1.36 (Poly/ML crash!?);
src/Pure/General/pretty.ML

2008-06-24 wenzelm [Tue, 24 Jun 2008 22:27:36 +0200] rev 27349
updated generated file;
doc-src/isabelle.sty

2008-06-24 wenzelm [Tue, 24 Jun 2008 22:13:19 +0200] rev 27348
YXML: no special treatment of white space;
doc-src/System/misc.tex

2008-06-24 wenzelm [Tue, 24 Jun 2008 21:44:52 +0200] rev 27347
pprint: proper output of markup (important for token translation);
src/Pure/General/pretty.ML

2008-06-24 wenzelm [Tue, 24 Jun 2008 19:43:22 +0200] rev 27346
ml_code_antiq: proper scanner combinators;
ML_Antiquote.value;
src/Tools/code/code_target.ML

2008-06-24 wenzelm [Tue, 24 Jun 2008 19:43:21 +0200] rev 27345
moved concrete antiquotations to ml_antiquote.ML;
src/Pure/Thy/thy_info.ML

2008-06-24 wenzelm [Tue, 24 Jun 2008 19:43:20 +0200] rev 27344
Antiquote.Open/Close;
src/Pure/Thy/latex.ML src/Pure/Thy/thy_output.ML