2014-05-16 blanchet [Fri, 16 May 2014 12:56:39 +0200] rev 56978
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

2014-05-16 nipkow [Fri, 16 May 2014 09:19:15 +0200] rev 56977
new syntax for card, normalized spacing for #
src/Doc/Sugar/Sugar.thy src/HOL/Library/LaTeXsugar.thy

2014-05-15 haftmann [Thu, 15 May 2014 16:46:29 +0200] rev 56976
clarified stylized status of sandwich algebra
src/Tools/Code/code_preproc.ML

2014-05-15 haftmann [Thu, 15 May 2014 16:38:33 +0200] rev 56975
dropped dead code
src/HOL/Tools/value.ML

2014-05-15 haftmann [Thu, 15 May 2014 16:38:32 +0200] rev 56974
accurate separation of static and dynamic context
src/Tools/nbe.ML

2014-05-15 haftmann [Thu, 15 May 2014 16:38:31 +0200] rev 56973
syntactic means to prevent accidental mixup of static and dynamic context
src/HOL/Tools/code_evaluation.ML src/Tools/Code/code_preproc.ML src/Tools/Code/code_runtime.ML src/Tools/Code/code_simp.ML src/Tools/Code/code_thingol.ML src/Tools/nbe.ML

2014-05-15 haftmann [Thu, 15 May 2014 16:38:31 +0200] rev 56972
proper separation of static and dynamic context
src/Tools/nbe.ML

2014-05-15 haftmann [Thu, 15 May 2014 16:38:30 +0200] rev 56971
optimization for trivial cases
src/Tools/Code/code_preproc.ML

2014-05-15 haftmann [Thu, 15 May 2014 16:38:29 +0200] rev 56970
modernized setup
src/Tools/Code/code_preproc.ML src/Tools/Code_Generator.thy

2014-05-15 haftmann [Thu, 15 May 2014 16:38:29 +0200] rev 56969
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
src/Tools/Code/code_runtime.ML src/Tools/Code/code_simp.ML src/Tools/Code/code_thingol.ML src/Tools/nbe.ML