boehmes [Tue, 20 Oct 2009 15:03:17 +0200] rev 33021
additional schematic rules for Z3's rewrite rule
nipkow [Tue, 20 Oct 2009 14:44:19 +0200] rev 33020
merged
nipkow [Tue, 20 Oct 2009 14:44:02 +0200] rev 33019
added Hilbert_Choice section
boehmes [Tue, 20 Oct 2009 14:22:54 +0200] rev 33018
merged
boehmes [Tue, 20 Oct 2009 14:22:02 +0200] rev 33017
eliminated extraneous wrapping of public records,
replaced simp_tac by best_tac (simplifier failed),
less strict condition for rewrite (can also handle equations with single literal on left-hand side)
boehmes [Tue, 20 Oct 2009 12:06:17 +0200] rev 33016
proper exceptions instead of unhandled partiality
nipkow [Tue, 20 Oct 2009 13:37:56 +0200] rev 33015
footnote: inv via inv_onto
nipkow [Tue, 20 Oct 2009 13:20:42 +0200] rev 33014
added inv_def for compatibility as a lemma
wenzelm [Tue, 20 Oct 2009 11:36:19 +0200] rev 33013
slightly less context-sensitive settings;
wenzelm [Tue, 20 Oct 2009 11:08:50 +0200] rev 33012
merged