| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 15:27:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 13:51:38 +0200 |
steckerm |
Fixed bug in waldmeister skolemization
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 20:14:04 +0200 |
wenzelm |
more standard Isabelle/ML operations;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 19:53:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:44:24 +0200 |
steckerm |
Removed double space
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:44:24 +0200 |
steckerm |
Minor fixes in ATP_Waldmeister
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:44:23 +0200 |
steckerm |
Made encoded type for apply less restrictive
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:44:23 +0200 |
steckerm |
Updated fix_name function
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Added support for partial function application
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Improved equality handling in skolemization
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Re-added hypothesis argument to problem generation
|
file |
diff |
annotate
|
| Sun, 07 Sep 2014 14:39:23 +0200 |
steckerm |
Added translation for lambda expressions in terms.
|
file |
diff |
annotate
|
| Tue, 02 Sep 2014 16:38:26 +0200 |
steckerm |
Some work on the new waldmeister integration
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 00:50:41 +0200 |
blanchet |
also try 'metis' with 'full_types'
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
more robust handling of types for skolems (modeled as Frees)
|
file |
diff |
annotate
|
| Tue, 17 Jun 2014 18:33:34 +0200 |
blanchet |
reintroduce atomize in Waldmeister code
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:42:44 +0200 |
blanchet |
integrated new Waldmeister code with 'sledgehammer' command
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:40:04 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
| base
|