src/HOL/SMT/Z3.thy
Tue, 20 Oct 2009 15:03:17 +0200 boehmes additional schematic rules for Z3's rewrite rule
Tue, 20 Oct 2009 10:11:30 +0200 boehmes added proof reconstructon for Z3,
less more (0) tip