isabelle update -u control_cartouches;

tuned;

tuned syntax -- more symbols;

more symbols;

modernized header uniformly as section;

more cartouches;

prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;

syntax translations always depend on context;

modernized dynamic "rules" -- avoid rebinding of static facts;

discontinued redundant ASCII syntax;

modernized specifications;

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

eliminated global prems;

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

--HG--
rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML

adapted to authentic syntax;

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};

modernized some syntax translations;

setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;

avoid internal names;

added header;

replaced _K by dummy abstraction;

tuned;

converted to Isar theory format;

renaming of theory LOmega to lomega2 in order to prevent a possible
case confusion

reorganized into individual theories;

"->" made syntax;

syntactic constants;

removed \...\ inside strings

removal of obsolete type-declaration syntax

replaced id by idt;
added parse rule for ->;
removed ndependent_tr;

Initial revision