2013-10-02 wenzelm [Wed, 02 Oct 2013 17:09:12 +0200] rev 54034
some highlights of Isabelle2013-1 based on NEWS;
ANNOUNCE

2013-10-02 wenzelm [Wed, 02 Oct 2013 17:08:39 +0200] rev 54033
tuned;
NEWS

2013-10-02 wenzelm [Wed, 02 Oct 2013 16:56:02 +0200] rev 54032
misc tuning for release;
NEWS

2013-10-02 blanchet [Wed, 02 Oct 2013 16:29:41 +0200] rev 54031
more (co)data docs
src/Doc/Datatypes/Datatypes.thy

2013-10-02 blanchet [Wed, 02 Oct 2013 16:29:40 +0200] rev 54030
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

2013-10-02 traytel [Wed, 02 Oct 2013 15:53:20 +0200] rev 54029
NEWS and CONTRIBUTORS
CONTRIBUTORS NEWS

2013-10-02 traytel [Wed, 02 Oct 2013 15:13:41 +0200] rev 54028
made SML/NJ happy
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

2013-10-02 traytel [Wed, 02 Oct 2013 13:29:04 +0200] rev 54027
use new coinduction method and primcorec in examples
src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy src/HOL/BNF/Examples/Koenig.thy src/HOL/BNF/Examples/Process.thy src/HOL/BNF/Examples/Stream.thy src/HOL/BNF/Examples/TreeFI.thy src/HOL/BNF/Examples/TreeFsetI.thy

2013-10-02 traytel [Wed, 02 Oct 2013 11:57:52 +0200] rev 54026
new coinduction method
src/HOL/BNF/BNF.thy src/HOL/BNF/Coinduction.thy src/HOL/BNF/Tools/coinduction.ML

2013-10-02 blanchet [Wed, 02 Oct 2013 10:53:15 +0200] rev 54025
tuned command descriptions
src/HOL/BNF/Tools/bnf_gfp.ML src/HOL/BNF/Tools/bnf_lfp.ML src/HOL/BNF/Tools/bnf_lfp_compat.ML