2013-12-09 haftmann [Mon, 09 Dec 2013 22:49:27 +0100] rev 54708
NEWS
NEWS

2013-12-07 haftmann [Sat, 07 Dec 2013 20:09:35 +0100] rev 54707
default code equations for make, fields, extend and truncate operations on records
src/HOL/Tools/record.ML

2013-12-09 wenzelm [Mon, 09 Dec 2013 21:32:45 +0100] rev 54706
browse directory hyperlink as well;
src/Tools/jEdit/src/jedit_editor.scala

2013-12-09 wenzelm [Mon, 09 Dec 2013 20:16:12 +0100] rev 54705
provide @{file_unchecked} in Isabelle/Pure;
NEWS src/Doc/IsarRef/Document_Preparation.thy src/Doc/System/Basics.thy src/Doc/System/Sessions.thy src/Doc/antiquote_setup.ML src/Pure/Thy/thy_load.ML

2013-12-09 wenzelm [Mon, 09 Dec 2013 12:27:18 +0100] rev 54704
tuned;
src/Doc/System/Sessions.thy

2013-12-09 wenzelm [Mon, 09 Dec 2013 12:22:23 +0100] rev 54703
more antiquotations;
src/Doc/IsarImplementation/ML.thy src/Doc/JEdit/JEdit.thy src/Doc/Locales/Examples3.thy src/Doc/Main/Main_Doc.thy src/Doc/ProgProve/Basics.thy src/Doc/System/Interfaces.thy src/Doc/System/Misc.thy src/Doc/System/Sessions.thy src/HOL/Bali/Decl.thy src/HOL/Groups.thy src/HOL/Imperative_HOL/Ref.thy src/HOL/Induct/Ordinals.thy src/HOL/Library/Binomial.thy src/HOL/Library/Kleene_Algebra.thy src/HOL/Library/State_Monad.thy src/HOL/Library/Sum_of_Squares.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Nominal/Examples/CK_Machine.thy src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy src/HOL/Real_Vector_Spaces.thy src/HOL/Rings.thy src/HOL/Series.thy src/HOL/ex/ML.thy src/HOL/ex/NatSum.thy src/HOL/ex/Sudoku.thy

2013-12-09 wenzelm [Mon, 09 Dec 2013 12:16:52 +0100] rev 54702
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
NEWS src/Doc/IsarRef/Document_Preparation.thy src/Pure/General/url.ML src/Pure/PIDE/editor.scala src/Pure/PIDE/markup.ML src/Pure/PIDE/markup.scala src/Pure/Thy/thy_output.ML src/Tools/jEdit/src/jedit_editor.scala src/Tools/jEdit/src/rendering.scala

2013-12-09 blanchet [Mon, 09 Dec 2013 09:44:57 +0100] rev 54701
tuning -- moved ML files to subdirectory
src/HOL/Ctr_Sugar.thy src/HOL/Tools/Ctr_Sugar/case_translation.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML src/HOL/Tools/case_translation.ML src/HOL/Tools/ctr_sugar.ML src/HOL/Tools/ctr_sugar_code.ML src/HOL/Tools/ctr_sugar_tactics.ML src/HOL/Tools/ctr_sugar_util.ML

2013-12-09 blanchet [Mon, 09 Dec 2013 06:33:46 +0100] rev 54700
adapted code for Z3 proof reconstruction
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML src/HOL/Tools/Sledgehammer/sledgehammer_print.ML src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML

2013-12-09 blanchet [Mon, 09 Dec 2013 05:06:48 +0100] rev 54699
useful debugging info
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML