boehmes [Mon, 04 Jun 2012 09:07:23 +0200] rev 49084
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"
haftmann [Sun, 03 Jun 2012 15:49:55 +0200] rev 49083
explicit check for correct number of arguments for abstract constructor
huffman [Sat, 02 Jun 2012 08:32:42 +0200] rev 49082
merged
huffman [Sat, 02 Jun 2012 08:27:29 +0200] rev 49081
transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman [Fri, 01 Jun 2012 11:55:06 +0200] rev 49080
transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman [Fri, 01 Jun 2012 11:54:34 +0200] rev 49079
unify theory-data structures for transfer package
huffman [Fri, 01 Jun 2012 11:53:58 +0200] rev 49078
remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
Andreas Lochbihler [Fri, 01 Jun 2012 20:40:34 +0200] rev 49077
improved code setup for card, finite, subset
Andreas Lochbihler [Fri, 01 Jun 2012 15:35:49 +0200] rev 49076
merged
Andreas Lochbihler [Fri, 01 Jun 2012 15:33:31 +0200] rev 49075
more instantiations for card_UNIV,
more lemmas for CARD