Fri, 11 Dec 2009 15:36:24 +0100 merged
boehmes [Fri, 11 Dec 2009 15:36:24 +0100] rev 34070
merged
Fri, 11 Dec 2009 15:36:05 +0100 updated dependencies
boehmes [Fri, 11 Dec 2009 15:36:05 +0100] rev 34069
updated dependencies
Fri, 11 Dec 2009 15:35:29 +0100 make assertion labels unique already when loading a verification condition,
boehmes [Fri, 11 Dec 2009 15:35:29 +0100] rev 34068
make assertion labels unique already when loading a verification condition, keep abstract view on verification conditions and provide various splitting operations on verification conditions, allow to discharge only parts of a verification condition, extended the command "boogie_vc" with options to consider only some assertions or to split a verification condition into its paths, added a narrowing option to "boogie_status" (a divide-and-conquer approach for identifying the "hard" subset of assertions of a verification conditions), added tactics "boogie", "boogie_all" and "boogie_cases", dropped tactic "split_vc", split example Boogie_Max into Boogie_Max (proof based on SMT) and Boogie_Max_Stepwise (proof based on metis and auto with documentation of the available Boogie commands), dropped (mostly unused) abbreviations
Fri, 11 Dec 2009 15:06:12 +0100 depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
boehmes [Fri, 11 Dec 2009 15:06:12 +0100] rev 34067
depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
Fri, 11 Dec 2009 14:44:08 +0100 merged
haftmann [Fri, 11 Dec 2009 14:44:08 +0100] rev 34066
merged
Fri, 11 Dec 2009 14:43:56 +0100 moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann [Fri, 11 Dec 2009 14:43:56 +0100] rev 34065
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
Fri, 11 Dec 2009 14:43:55 +0100 avoid dependency on implicit dest rule predicate1D in proofs
haftmann [Fri, 11 Dec 2009 14:43:55 +0100] rev 34064
avoid dependency on implicit dest rule predicate1D in proofs
Fri, 11 Dec 2009 14:32:37 +0100 merged
haftmann [Fri, 11 Dec 2009 14:32:37 +0100] rev 34063
merged
Fri, 11 Dec 2009 14:32:24 +0100 NEWS
haftmann [Fri, 11 Dec 2009 14:32:24 +0100] rev 34062
NEWS
Fri, 11 Dec 2009 08:47:16 +0100 merged
haftmann [Fri, 11 Dec 2009 08:47:16 +0100] rev 34061
merged
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip