2014-05-16 blanchet [Fri, 16 May 2014 19:13:50 +0200] rev 56981
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
src/HOL/Tools/SMT2/smt2_normalize.ML src/HOL/Tools/SMT2/smt2_solver.ML src/HOL/Tools/SMT2/z3_new_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML

2014-05-16 wenzelm [Fri, 16 May 2014 17:11:56 +0200] rev 56980
proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
src/Tools/jEdit/src/rendering.scala

2014-05-16 noschinl [Fri, 16 May 2014 16:40:02 +0200] rev 56979
added lemmas for -1
src/HOL/Word/Word.thy

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