2011-04-08 wenzelm [Fri, 08 Apr 2011 13:59:28 +0200] rev 42285
removed outdated text (cf. 84a3f86441eb);
src/HOL/Library/BigO.thy

2011-04-08 wenzelm [Fri, 08 Apr 2011 13:31:16 +0200] rev 42284
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;
NEWS src/CCL/Term.thy src/CCL/Type.thy src/Cube/Cube.thy src/FOLP/simp.ML src/HOL/Big_Operators.thy src/HOL/Complete_Lattice.thy src/HOL/Decision_Procs/Cooper.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/HOL.thy src/HOL/HOLCF/Cfun.thy src/HOL/HOLCF/ex/Pattern_Match.thy src/HOL/Hilbert_Choice.thy src/HOL/Hoare/hoare_syntax.ML src/HOL/Hoare_Parallel/OG_Syntax.thy src/HOL/Hoare_Parallel/Quote_Antiquote.thy src/HOL/Hoare_Parallel/RG_Syntax.thy src/HOL/Isar_Examples/Hoare.thy src/HOL/Library/reflection.ML src/HOL/Orderings.thy src/HOL/Product_Type.thy src/HOL/Set.thy src/HOL/Tools/Datatype/datatype_case.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/record.ML src/HOL/ex/Antiquote.thy src/Pure/IsaMakefile src/Pure/Isar/attrib.ML src/Pure/Isar/obtain.ML src/Pure/ProofGeneral/preferences.ML src/Pure/ROOT.ML src/Pure/Syntax/local_syntax.ML src/Pure/Syntax/mixfix.ML src/Pure/Syntax/printer.ML src/Pure/Syntax/syn_trans.ML src/Pure/Syntax/syntax.ML src/Pure/Syntax/syntax_phases.ML src/Pure/Syntax/syntax_trans.ML src/Pure/Thy/thy_output.ML src/Pure/primitive_defs.ML src/Pure/pure_thy.ML src/Pure/raw_simplifier.ML src/Pure/sign.ML src/Pure/type_infer.ML src/Tools/Code/code_thingol.ML src/Tools/induct.ML src/Tools/misc_legacy.ML src/Tools/subtyping.ML

2011-04-08 wenzelm [Fri, 08 Apr 2011 11:39:45 +0200] rev 42283
tuned presentation;
src/Tools/jEdit/src/jedit/isabelle_markup.scala

2011-04-07 wenzelm [Thu, 07 Apr 2011 23:25:09 +0200] rev 42282
report literal tokens according to parsetree head;
some attempts to stack parsetrees in proper order;
src/Pure/Syntax/parser.ML src/Pure/Syntax/syntax_phases.ML

2011-04-07 wenzelm [Thu, 07 Apr 2011 21:55:09 +0200] rev 42281
simplified read_term vs. read_prop;
src/Pure/Syntax/syntax_phases.ML

2011-04-07 wenzelm [Thu, 07 Apr 2011 21:37:42 +0200] rev 42280
tuned signature;
src/Pure/Syntax/syntax.ML

2011-04-07 wenzelm [Thu, 07 Apr 2011 21:23:57 +0200] rev 42279
constant =?= no longer exists (cf. 8c09e1fa24a7);
doc-src/IsarRef/Thy/Inner_Syntax.thy doc-src/IsarRef/Thy/document/Inner_Syntax.tex src/Pure/Syntax/simple_syntax.ML src/Pure/unify.ML

2011-04-07 wenzelm [Thu, 07 Apr 2011 20:56:48 +0200] rev 42278
clarified sources -- removed odd comments;
src/Pure/Syntax/syn_trans.ML

2011-04-07 wenzelm [Thu, 07 Apr 2011 20:32:42 +0200] rev 42277
tuned signature;
src/Pure/Isar/attrib.ML src/Pure/Syntax/ast.ML

2011-04-07 wenzelm [Thu, 07 Apr 2011 18:41:49 +0200] rev 42276
merged
src/Pure/Syntax/type_ext.ML