| Tue, 15 Jan 2013 16:34:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 09 Jan 2013 20:46:32 +0100 |
smolkas |
changed exception to uppercase
|
file |
diff |
annotate
|
| Wed, 09 Jan 2013 20:29:50 +0100 |
smolkas |
proper exception handling; reraise interrupt exceptions
|
file |
diff |
annotate
|
| Wed, 09 Jan 2013 14:36:24 +0100 |
smolkas |
consider merging obtain steps
|
file |
diff |
annotate
|
| Wed, 09 Jan 2013 14:35:46 +0100 |
smolkas |
preplay obtain steps
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 15:05:48 +0100 |
smolkas |
tuned
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 20:52:32 +0100 |
smolkas |
removed duplicate code
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 15:44:00 +0100 |
blanchet |
added "obtain" to Isar proof construction data structure
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
improved readability
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
fixed case split preplaying
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
preplay case splits
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
deal with the case that metis does not time out, but fails instead
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
reapplied changes to make SML/NJ happy
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
renaming, minor tweaks, added signature
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
made use of sledgehammer_util
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
added comments to new source files
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:06 +0100 |
smolkas |
remove hack and generalize code slightly
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:23:44 +0100 |
smolkas |
simplified isar_qualifiers and qs merging
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:22:17 +0100 |
smolkas |
put shrink in own structure
|
file |
diff |
annotate
|