| Fri, 12 Jul 2013 19:54:36 +0200 |
smolkas |
tuned
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 18:44:59 +0200 |
smolkas |
moved code -> easier debugging
|
file |
diff |
annotate
|
| Wed, 26 Jun 2013 18:24:41 +0200 |
smolkas |
ommit trivial tfrees in annotations
|
file |
diff |
annotate
|
| Tue, 11 Jun 2013 19:58:09 -0400 |
smolkas |
uncheck terms before annotation to avoid awkward syntax
|
file |
diff |
annotate
|
| Tue, 11 Jun 2013 16:13:19 -0400 |
smolkas |
make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
|
file |
diff |
annotate
|
| Wed, 22 May 2013 12:39:09 +0200 |
smolkas |
prevent pretty printer from automatically annotating numerals
|
file |
diff |
annotate
|
| Mon, 06 May 2013 11:03:08 +0200 |
smolkas |
avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 12:16:27 +0100 |
smolkas |
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
|
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:22:17 +0100 |
smolkas |
put shrink in own structure
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:22:05 +0100 |
smolkas |
put annotate in own structure
|
file |
diff |
annotate
|