wenzelm [Wed, 25 Jun 2008 21:25:51 +0200] rev 27361
modernized specifications;
urbanc [Wed, 25 Jun 2008 18:23:50 +0200] rev 27360
typo
wenzelm [Wed, 25 Jun 2008 17:38:39 +0200] rev 27359
re-use official outer keywords;
wenzelm [Wed, 25 Jun 2008 17:38:38 +0200] rev 27358
scan: prefer command over keyword, allowing lexicons to overlap;
wenzelm [Wed, 25 Jun 2008 17:38:37 +0200] rev 27357
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
lexicons: allow overlapping keywords/commands -- warning instead of error;
wenzelm [Wed, 25 Jun 2008 17:38:36 +0200] rev 27356
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
moved check_text here;
wenzelm [Wed, 25 Jun 2008 17:38:35 +0200] rev 27355
antiquote: need to quote outer keywords;
wenzelm [Wed, 25 Jun 2008 17:38:34 +0200] rev 27354
tuned;
wenzelm [Wed, 25 Jun 2008 17:38:32 +0200] rev 27353
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
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