| Sun, 28 Aug 2011 14:50:13 +0100 |
Christian Urban |
updated to Isabelle 28 Aug
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 22:56:07 +0200 |
Christian Urban |
made same changes as in main branch
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 17:42:35 +0200 |
Christian Urban |
uodated to new Isabelle (15. Aug)
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 01:40:36 +0100 |
Christian Urban |
generated the partial eqvt-theorem for functions
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 17:40:13 +0100 |
Christian Urban |
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
|
file |
diff |
annotate
|
| Thu, 16 Jun 2011 13:14:16 +0100 |
Christian Urban |
added eqvt_at and invariant for boths sides of the equations
|
file |
diff |
annotate
|
| Thu, 16 Jun 2011 12:12:25 +0100 |
Christian Urban |
added a test that every function must be of pt-sort
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 08:52:59 +0100 |
Christian Urban |
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
|
file |
diff |
annotate
|
| Sun, 05 Jun 2011 21:14:23 +0100 |
Christian Urban |
added an option for an invariant (at the moment only a stub)
|
file |
diff |
annotate
|
| Tue, 31 May 2011 00:17:22 +0100 |
Christian Urban |
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 13:47:08 +0100 |
Christian Urban |
changed default preprocessor that does not catch variables only occuring on the right
|
file |
diff |
annotate
|
| Wed, 16 Mar 2011 20:42:14 +0100 |
Christian Urban |
ported changes from function package....needs Isabelle 16 March or above
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 14:37:18 +0100 |
Christian Urban |
exported nominal function code to external file
|
file |
diff |
annotate
|