Mon, 19 Apr 2010 11:04:31 +0200 |
Cezary Kaliszyk |
2 more lifted lemmas needed for second representation
|
changeset |
files
|
Mon, 19 Apr 2010 10:35:08 +0200 |
Cezary Kaliszyk |
Accept non-equality eqvt rules in support proofs.
|
changeset |
files
|
Mon, 19 Apr 2010 10:00:52 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Mon, 19 Apr 2010 09:59:32 +0200 |
Cezary Kaliszyk |
Locations of files in Parser
|
changeset |
files
|
Mon, 19 Apr 2010 09:25:55 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Mon, 19 Apr 2010 09:25:43 +0200 |
Cezary Kaliszyk |
minor FSet3 edits.
|
changeset |
files
|
Sun, 18 Apr 2010 18:01:22 +0200 |
Christian Urban |
tuned
|
changeset |
files
|
Sun, 18 Apr 2010 17:58:45 +0200 |
Christian Urban |
moved some general function into nominal_library.ML
|
changeset |
files
|
Sun, 18 Apr 2010 17:57:27 +0200 |
Christian Urban |
tuned; transformation functions now take a context, a thm and return a thm
|
changeset |
files
|
Sun, 18 Apr 2010 17:56:05 +0200 |
Christian Urban |
tuned
|
changeset |
files
|
Sun, 18 Apr 2010 10:58:29 +0200 |
Christian Urban |
equivariance for alpha_raw in CoreHaskell is automatically derived
|
changeset |
files
|
Sun, 18 Apr 2010 09:26:38 +0200 |
Christian Urban |
preliminary parser for perm_simp metod
|
changeset |
files
|
Fri, 16 Apr 2010 16:29:11 +0200 |
Christian Urban |
automatic proofs for equivariance of alphas
|
changeset |
files
|
Fri, 16 Apr 2010 11:09:32 +0200 |
Cezary Kaliszyk |
Finished proof in Lambda.thy
|
changeset |
files
|