| Thu, 03 Mar 2011 18:10:28 +0100 |
wenzelm |
discontinued legacy load path;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 18:18:42 +0100 |
wenzelm |
theory loader: implicit load path is considered legacy;
|
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
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:49:07 +0200 |
blanchet |
move Meson to Plain
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 17:56:41 +0200 |
haftmann |
group record-related ML files
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:11:37 +0100 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 20:30:17 +0100 |
haftmann |
moved instance option :: finite to Option.thy
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 07:58:13 -0800 |
huffman |
change imports to move Fact.thy outside Plain
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 15:38:26 +0000 |
chaieb |
Now imports Fact as suggested by Florian in order to avoid the typerep problem
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 13:43:19 +0100 |
blanchet |
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
changed import hierarchy
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 00:21:59 +0100 |
wenzelm |
tuned header and description of boot files;
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|