| Mon, 19 Apr 2010 16:33:48 +0200 |
got rid of somewhat pointless "pairname" function in Sledgehammer
|
file | diff | annotate |
| Sun, 11 Apr 2010 14:30:34 +0200 |
Thm.add_axiom/add_def: return internal name of foundational axiom;
|
file | diff | annotate |
| Sat, 27 Mar 2010 14:10:37 +0100 |
eliminated old-style Theory.add_defs_i;
|
file | diff | annotate |
| Thu, 25 Mar 2010 17:55:55 +0100 |
make Mirabelle happy again
|
file | diff | annotate |
| Tue, 23 Mar 2010 11:39:21 +0100 |
added options to Sledgehammer;
|
file | diff | annotate |
| Mon, 22 Mar 2010 10:25:44 +0100 |
merged
|
file | diff | annotate |
| Mon, 22 Mar 2010 10:25:07 +0100 |
start work on direct proof reconstruction for Sledgehammer
|
file | diff | annotate |
| Fri, 19 Mar 2010 13:02:18 +0100 |
more Sledgehammer refactoring
|
file | diff | annotate |
| Sat, 20 Mar 2010 17:33:11 +0100 |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file | diff | annotate |
| Thu, 18 Mar 2010 12:58:52 +0100 |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file | diff | annotate |
| Wed, 17 Mar 2010 19:26:05 +0100 |
renamed Sledgehammer structures
|
file | diff | annotate |
| Wed, 17 Mar 2010 18:16:31 +0100 |
move Sledgehammer files in a directory of their own
|
file | diff | annotate | base |