| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
rename lambda translation schemes
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 17:59:58 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
Metis code cleanup
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
more preparations towards hijacking Metis
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 17:10:27 +0200 |
wenzelm |
prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:43:50 +0100 |
blanchet |
fix Mirabelle after renaming Sledgehammer structures
|
file |
diff |
annotate
|
| Sun, 13 Sep 2009 02:10:41 +0200 |
wenzelm |
explicitly export type abbreviations (as usual in SML97);
|
file |
diff |
annotate
|
| Sat, 12 Sep 2009 16:30:48 +0200 |
wenzelm |
standard headers and text sections;
|
file |
diff |
annotate
|
| Fri, 11 Sep 2009 09:52:40 +0200 |
nipkow |
Made record parameter flexible to allow for extensions
|
file |
diff |
annotate
|
| Sat, 05 Sep 2009 11:45:57 +0200 |
boehmes |
added initialization and cleanup of actions,
|
file |
diff |
annotate
|
| Fri, 04 Sep 2009 13:57:56 +0200 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 22:47:31 +0200 |
boehmes |
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 21:31:58 +0200 |
boehmes |
Mirabelle: actions are responsible for handling exceptions,
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 16:23:53 +0200 |
boehmes |
moved Mirabelle from HOL/Tools to HOL,
|
file |
diff |
annotate
| base
|