2013-11-10 haftmann [Sun, 10 Nov 2013 10:02:34 +0100] rev 54293
simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number
src/HOL/Tools/SMT/smt_normalize.ML

2013-11-08 nipkow [Fri, 08 Nov 2013 21:40:07 +0100] rev 54292
more exercises
src/Doc/ProgProve/Isar.thy src/Doc/ProgProve/Logic.thy

2013-11-08 blanchet [Fri, 08 Nov 2013 19:03:14 +0100] rev 54291
by (auto ...)[1] not by (auto [1])
src/HOL/Tools/try0.ML

2013-11-08 nipkow [Fri, 08 Nov 2013 08:59:54 +0100] rev 54290
added exercise
src/Doc/ProgProve/Logic.thy

2013-11-07 kleing [Thu, 07 Nov 2013 16:08:19 +1100] rev 54289
Add output translation for <a := .., b := .., ..> state notation.
src/HOL/IMP/AExp.thy

2013-11-07 blanchet [Thu, 07 Nov 2013 02:42:20 +0100] rev 54288
reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables)
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML

2013-11-07 blanchet [Thu, 07 Nov 2013 01:01:04 +0100] rev 54287
more docs
src/Doc/Datatypes/Datatypes.thy

2013-11-07 blanchet [Thu, 07 Nov 2013 00:37:18 +0100] rev 54286
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML src/HOL/BNF/Tools/bnf_lfp_compat.ML

2013-11-06 blanchet [Wed, 06 Nov 2013 23:05:44 +0100] rev 54285
reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP
src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/ctr_sugar.ML

2013-11-06 blanchet [Wed, 06 Nov 2013 22:50:12 +0100] rev 54284
simplified code
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML