2013-04-26 blanchet [Fri, 26 Apr 2013 12:09:51 +0200] rev 51790
more intuitive syntax for equality-style discriminators of nullary constructors
src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_util.ML src/HOL/BNF/Tools/bnf_wrap.ML

2013-04-26 blanchet [Fri, 26 Apr 2013 11:04:47 +0200] rev 51789
updated keywords
etc/isar-keywords.el

2013-04-26 blanchet [Fri, 26 Apr 2013 11:04:46 +0200] rev 51788
put an underscore in prefix
src/HOL/BNF/Examples/Stream.thy src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

2013-04-26 blanchet [Fri, 26 Apr 2013 11:04:45 +0200] rev 51787
changed discriminator default: avoid mixing ctor and dtor views
src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_util.ML src/HOL/BNF/Tools/bnf_wrap.ML

2013-04-26 nipkow [Fri, 26 Apr 2013 09:53:11 +0200] rev 51786
simplified def
src/HOL/IMP/Abs_Int1.thy src/HOL/IMP/Abs_Int3.thy

2013-04-26 nipkow [Fri, 26 Apr 2013 09:41:45 +0200] rev 51785
more standard order of arguments
src/HOL/IMP/Abs_Int0.thy src/HOL/IMP/Abs_Int1.thy src/HOL/IMP/Abs_Int2.thy src/HOL/IMP/Abs_Int3.thy

2013-04-26 nipkow [Fri, 26 Apr 2013 09:01:45 +0200] rev 51784
more funs
src/Doc/ProgProve/Logic.thy src/Doc/ProgProve/document/root.bib

2013-04-26 nipkow [Fri, 26 Apr 2013 07:49:38 +0200] rev 51783
simplified def
src/HOL/IMP/Abs_Int0.thy

2013-04-25 traytel [Thu, 25 Apr 2013 19:18:20 +0200] rev 51782
removed unnecessary assumptions in some theorems about cardinal exponentiation
src/HOL/BNF/BNF_GFP.thy src/HOL/BNF/Basic_BNFs.thy src/HOL/BNF/More_BNFs.thy src/HOL/BNF/Tools/bnf_comp.ML src/HOL/BNF/Tools/bnf_comp_tactics.ML src/HOL/BNF/Tools/bnf_gfp.ML src/HOL/BNF/Tools/bnf_gfp_tactics.ML src/HOL/BNF/Tools/bnf_lfp.ML src/HOL/BNF/Tools/bnf_lfp_tactics.ML src/HOL/Cardinals/Cardinal_Arithmetic.thy

2013-04-25 blanchet [Thu, 25 Apr 2013 18:27:26 +0200] rev 51781
renamed "wrap_data" to "wrap_free_constructors"
src/HOL/BNF/BNF_Wrap.thy src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_wrap.ML