| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
made BNF compile after move to HOL
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
moved BNF files to 'HOL'
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:55 +0100 |
blanchet |
kill notations
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:55 +0100 |
blanchet |
renamed '_FP' files to 'BNF_' files
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:55 +0100 |
blanchet |
moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
|
file |
diff |
annotate
|
| Thu, 16 Jan 2014 16:33:19 +0100 |
blanchet |
moved 'Zorn' into 'Main', since it's a BNF dependency
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 20:45:20 +0100 |
blanchet |
moved 'coinduction' proof method to 'HOL'
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 18:58:00 +0100 |
blanchet |
factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 12:24:42 +0100 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
| Sat, 07 Jan 2012 20:18:56 +0100 |
haftmann |
dropped theory More_Set
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 22:17:10 +0100 |
haftmann |
incorporated More_Set and More_List into the Main body -- to be consolidated later
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 16:21:48 +0200 |
noschinl |
tune simpset for Complete_Lattices
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 01:33:58 +0200 |
haftmann |
compatibility layer
|
file |
diff |
annotate
|
| Thu, 05 May 2011 10:47:31 +0200 |
bulwahn |
adding creation of exhaustive generators for records; simplifying dependencies in Main theory
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
correcting dependencies after renaming
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 09:25:43 +0100 |
bulwahn |
adding code and theory for smallvalue generators, but do not setup the interpretation yet
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 13:16:43 +0200 |
blanchet |
integrated "smt" proof method with Sledgehammer
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:17:19 +0200 |
blanchet |
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:57 +0200 |
haftmann |
moved sledgehammer to Plain; tuned dependencies
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 17:56:41 +0200 |
haftmann |
group record-related ML files
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 19:31:00 +0100 |
blanchet |
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 15:06:38 +0100 |
blanchet |
reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 12:29:31 +0100 |
blanchet |
readded Predicate_Compile to Main
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 18:09:30 +0100 |
blanchet |
merged my Auto Nitpick change with Lukas's Predicate Compiler changes
|
file |
diff |
annotate
|