| Sun, 26 Jun 2011 17:55:22 +0100 |
Christian Urban |
another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 22:51:43 +0100 |
Christian Urban |
did all cases, except the multiple binder case
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 21:28:24 +0100 |
Christian Urban |
an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders.
|
file |
diff |
annotate
|
| Fri, 24 Jun 2011 09:42:44 +0100 |
Christian Urban |
except for the interated binder case, finished definition in Calssical.thy
|
file |
diff |
annotate
|
| Fri, 24 Jun 2011 10:12:47 +0900 |
Cezary Kaliszyk |
Speed-up the completeness proof.
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 22:21:43 +0100 |
Christian Urban |
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 12:28:25 +0100 |
Christian Urban |
expanded the example
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 09:13:25 +0000 |
Christian Urban |
properly exported strong exhaust theorem; cleaned up some examples
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 13:36:03 +0800 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 02:08:00 +0800 |
Christian Urban |
cleaned up (almost completely) the examples
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 22:55:42 +0800 |
Christian Urban |
automatic lifting
|
file |
diff |
annotate
|
| Mon, 07 Jun 2010 11:43:01 +0200 |
Christian Urban |
work on transitivity proof
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 11:37:51 +0200 |
Christian Urban |
fixed problem with bn_info
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:59:53 +0100 |
Christian Urban |
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:57:01 +0200 |
Cezary Kaliszyk |
include set_simps and append_simps in fv_rsp
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:32:44 +0200 |
Cezary Kaliszyk |
Use equivariance instead of alpha_eqvt
|
file |
diff |
annotate
|