| Mon, 17 May 2010 16:25:45 +0100 |
Christian Urban |
minor tuning
|
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:33:25 +0100 |
Christian Urban |
moved the data-transformation into the parser
|
file |
diff |
annotate
|
| Wed, 12 May 2010 14:47:52 +0100 |
Christian Urban |
ingnored parameters in equivariance; added a proper interface to be called from ML
|
file |
diff |
annotate
|
| Wed, 12 May 2010 13:43:48 +0100 |
Christian Urban |
properly exported defined bn-functions
|
file |
diff |
annotate
|
| Tue, 11 May 2010 18:20:25 +0200 |
Cezary Kaliszyk |
Include raw permutation definitions in eqvt
|
file |
diff |
annotate
|
| Tue, 11 May 2010 17:16:57 +0200 |
Cezary Kaliszyk |
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
|
file |
diff |
annotate
|
| Wed, 05 May 2010 10:24:54 +0100 |
Christian Urban |
solved the problem with equivariance by first eta-normalising the goal
|
file |
diff |
annotate
|
| Mon, 03 May 2010 15:36:47 +0200 |
Cezary Kaliszyk |
SingleLet and Ex3 work with NewParser.
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:03:30 +0200 |
Cezary Kaliszyk |
Equivariance fails for single let?
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 18:24:50 +0200 |
Christian Urban |
renamed Ex1.thy to SingleLet.thy
|
file |
diff |
annotate
| base
|