2012-06-05 haftmann [Tue, 05 Jun 2012 07:05:56 +0200] rev 48072
prefer records with speaking labels over deeply nested tuples
src/HOL/Imperative_HOL/Heap_Monad.thy src/HOL/Tools/list_code.ML src/HOL/Tools/numeral.ML src/HOL/Tools/string_code.ML src/Tools/Code/code_haskell.ML src/Tools/Code/code_ml.ML src/Tools/Code/code_printer.ML src/Tools/Code/code_scala.ML src/Tools/Code/code_simp.ML src/Tools/Code/code_thingol.ML src/Tools/nbe.ML

2012-06-04 Andreas Lochbihler [Mon, 04 Jun 2012 12:55:54 +0200] rev 48071
merged

2012-06-04 Andreas Lochbihler [Mon, 04 Jun 2012 09:50:57 +0200] rev 48070
more sort constraints for FinFun code generation
src/HOL/Library/Cardinality.thy src/HOL/Library/FinFun.thy

2012-06-04 boehmes [Mon, 04 Jun 2012 09:07:23 +0200] rev 48069
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
NEWS src/HOL/Boogie/Examples/VCC_Max.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/SMT_Examples/SMT_Examples.thy src/HOL/SMT_Examples/SMT_Tests.thy src/HOL/Tools/SMT/smt_setup_solvers.ML

2012-06-03 haftmann [Sun, 03 Jun 2012 15:49:55 +0200] rev 48068
explicit check for correct number of arguments for abstract constructor
src/Pure/Isar/code.ML

2012-06-02 huffman [Sat, 02 Jun 2012 08:32:42 +0200] rev 48067
merged
src/HOL/Library/Cardinality.thy

2012-06-02 huffman [Sat, 02 Jun 2012 08:27:29 +0200] rev 48066
transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
src/HOL/Int.thy src/HOL/Tools/transfer.ML

2012-06-01 huffman [Fri, 01 Jun 2012 11:55:06 +0200] rev 48065
transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
src/HOL/Tools/transfer.ML

2012-06-01 huffman [Fri, 01 Jun 2012 11:54:34 +0200] rev 48064
unify theory-data structures for transfer package
src/HOL/Tools/transfer.ML

2012-06-01 huffman [Fri, 01 Jun 2012 11:53:58 +0200] rev 48063
remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
src/HOL/Finite_Set.thy src/HOL/Library/Cardinality.thy src/HOL/Library/Numeral_Type.thy