Tue, 05 Jun 2012 07:05:56 +0200 prefer records with speaking labels over deeply nested tuples
haftmann [Tue, 05 Jun 2012 07:05:56 +0200] rev 48072
prefer records with speaking labels over deeply nested tuples
Mon, 04 Jun 2012 12:55:54 +0200 merged
Andreas Lochbihler [Mon, 04 Jun 2012 12:55:54 +0200] rev 48071
merged
Mon, 04 Jun 2012 09:50:57 +0200 more sort constraints for FinFun code generation
Andreas Lochbihler [Mon, 04 Jun 2012 09:50:57 +0200] rev 48070
more sort constraints for FinFun code generation
Mon, 04 Jun 2012 09:07:23 +0200 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"
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"
Sun, 03 Jun 2012 15:49:55 +0200 explicit check for correct number of arguments for abstract constructor
haftmann [Sun, 03 Jun 2012 15:49:55 +0200] rev 48068
explicit check for correct number of arguments for abstract constructor
Sat, 02 Jun 2012 08:32:42 +0200 merged
huffman [Sat, 02 Jun 2012 08:32:42 +0200] rev 48067
merged
Sat, 02 Jun 2012 08:27:29 +0200 transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
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
Fri, 01 Jun 2012 11:55:06 +0200 transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
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
Fri, 01 Jun 2012 11:54:34 +0200 unify theory-data structures for transfer package
huffman [Fri, 01 Jun 2012 11:54:34 +0200] rev 48064
unify theory-data structures for transfer package
Fri, 01 Jun 2012 11:53:58 +0200 remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
huffman [Fri, 01 Jun 2012 11:53:58 +0200] rev 48063
remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
Fri, 01 Jun 2012 20:40:34 +0200 improved code setup for card, finite, subset
Andreas Lochbihler [Fri, 01 Jun 2012 20:40:34 +0200] rev 48062
improved code setup for card, finite, subset
Fri, 01 Jun 2012 15:35:49 +0200 merged
Andreas Lochbihler [Fri, 01 Jun 2012 15:35:49 +0200] rev 48061
merged
Fri, 01 Jun 2012 15:33:31 +0200 more instantiations for card_UNIV,
Andreas Lochbihler [Fri, 01 Jun 2012 15:33:31 +0200] rev 48060
more instantiations for card_UNIV, more lemmas for CARD
Fri, 01 Jun 2012 14:34:46 +0200 simplify card_UNIV type class,
Andreas Lochbihler [Fri, 01 Jun 2012 14:34:46 +0200] rev 48059
simplify card_UNIV type class, tuned proofs
Fri, 01 Jun 2012 13:52:51 +0200 drop redundant sort constraint
Andreas Lochbihler [Fri, 01 Jun 2012 13:52:51 +0200] rev 48058
drop redundant sort constraint
Fri, 01 Jun 2012 13:39:14 +0200 use \tocentry as in implementation manual;
wenzelm [Fri, 01 Jun 2012 13:39:14 +0200] rev 48057
use \tocentry as in implementation manual;
Fri, 01 Jun 2012 13:02:09 +0200 tuned message;
wenzelm [Fri, 01 Jun 2012 13:02:09 +0200] rev 48056
tuned message;
Fri, 01 Jun 2012 12:45:22 +0200 tuned header;
wenzelm [Fri, 01 Jun 2012 12:45:22 +0200] rev 48055
tuned header;
Fri, 01 Jun 2012 08:32:26 +0200 merged
Andreas Lochbihler [Fri, 01 Jun 2012 08:32:26 +0200] rev 48054
merged
Thu, 31 May 2012 17:10:43 +0200 tuned proofs
Andreas Lochbihler [Thu, 31 May 2012 17:10:43 +0200] rev 48053
tuned proofs
Thu, 31 May 2012 17:04:11 +0200 tuned instantiations
Andreas Lochbihler [Thu, 31 May 2012 17:04:11 +0200] rev 48052
tuned instantiations dropped redundant lemmas
Thu, 31 May 2012 16:58:38 +0200 unify Card_Univ and Cardinality
Andreas Lochbihler [Thu, 31 May 2012 16:58:38 +0200] rev 48051
unify Card_Univ and Cardinality
Thu, 31 May 2012 15:47:06 +0200 definition less_int_def has changed, use 'less_le' instead
huffman [Thu, 31 May 2012 15:47:06 +0200] rev 48050
definition less_int_def has changed, use 'less_le' instead
Mon, 28 May 2012 02:18:46 +0200 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn [Mon, 28 May 2012 02:18:46 +0200] rev 48049
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
Thu, 31 May 2012 10:05:07 +0200 remove stray reference to no-longer-existing theorem 'add'
huffman [Thu, 31 May 2012 10:05:07 +0200] rev 48048
remove stray reference to no-longer-existing theorem 'add'
Thu, 31 May 2012 10:01:15 +0200 temporarily comment out portion of Quotient_Examples/Quotient_Rat.thy, broken by changes to Int.thy
huffman [Thu, 31 May 2012 10:01:15 +0200] rev 48047
temporarily comment out portion of Quotient_Examples/Quotient_Rat.thy, broken by changes to Int.thy
Wed, 30 May 2012 18:09:23 +0200 temporarily comment out nitpick examples broken by changes to Int.thy
huffman [Wed, 30 May 2012 18:09:23 +0200] rev 48046
temporarily comment out nitpick examples broken by changes to Int.thy
Wed, 30 May 2012 16:59:20 +0200 convert Int.thy to use lifting and transfer
huffman [Wed, 30 May 2012 16:59:20 +0200] rev 48045
convert Int.thy to use lifting and transfer
Wed, 30 May 2012 14:55:44 +0200 remove unnecessary simp rules involving Abs_Integ
huffman [Wed, 30 May 2012 14:55:44 +0200] rev 48044
remove unnecessary simp rules involving Abs_Integ
Wed, 30 May 2012 23:10:42 +0200 introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes [Wed, 30 May 2012 23:10:42 +0200] rev 48043
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip