| 2010-06-22 |
Christian Urban |
proved eqvip theorems for alphas
|
file |
diff |
annotate
|
| 2010-06-22 |
Christian Urban |
prove that alpha implies alpha_bn (needed for rsp proofs)
|
file |
diff |
annotate
|
| 2010-06-21 |
Christian Urban |
merged with main line
|
file |
diff |
annotate
|
| 2010-06-11 |
Christian Urban |
also symmetry
|
file |
diff |
annotate
|
| 2010-06-09 |
Christian Urban |
transitivity proofs done
|
file |
diff |
annotate
|
| 2010-06-07 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| 2010-06-07 |
Christian Urban |
work on transitivity proof
|
file |
diff |
annotate
|
| 2010-06-02 |
Christian Urban |
fixed problem with bn_info
|
file |
diff |
annotate
|
| 2010-06-01 |
Christian Urban |
equivariance done
|
file |
diff |
annotate
|
| 2010-06-01 |
Christian Urban |
smaller code for raw-eqvt proofs
|
file |
diff |
annotate
|
| 2010-05-31 |
Christian Urban |
all raw definitions are defined using function
|
file |
diff |
annotate
|
| 2010-05-27 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| 2010-05-27 |
Christian Urban |
intermediate state
|
file |
diff |
annotate
|
| 2010-05-24 |
Christian Urban |
added slides
|
file |
diff |
annotate
|
| 2010-05-24 |
Christian Urban |
alpha works now
|
file |
diff |
annotate
|
| 2010-05-23 |
Christian Urban |
started to work on alpha
|
file |
diff |
annotate
|
| 2010-05-22 |
Christian Urban |
properly exported bn_descr
|
file |
diff |
annotate
|
| 2010-05-21 |
Christian Urban |
hving a working fv-definition without the export
|
file |
diff |
annotate
|
| 2010-05-21 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| 2010-05-20 |
Christian Urban |
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
|
file |
diff |
annotate
|
| 2010-06-20 |
Christian Urban |
fixed example
|
file |
diff |
annotate
|
| 2010-06-07 |
Christian Urban |
improved abstract, some tuning
|
file |
diff |
annotate
|
| 2010-05-27 |
Christian Urban |
fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
|
file |
diff |
annotate
|
| 2010-05-17 |
Christian Urban |
minor tuning
|
file |
diff |
annotate
|
| 2010-05-12 |
Christian Urban |
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
|
file |
diff |
annotate
|
| 2010-05-12 |
Christian Urban |
moved the data-transformation into the parser
|
file |
diff |
annotate
|
| 2010-05-12 |
Christian Urban |
ingnored parameters in equivariance; added a proper interface to be called from ML
|
file |
diff |
annotate
|
| 2010-05-12 |
Christian Urban |
properly exported defined bn-functions
|
file |
diff |
annotate
|
| 2010-05-11 |
Cezary Kaliszyk |
Include raw permutation definitions in eqvt
|
file |
diff |
annotate
|
| 2010-05-11 |
Cezary Kaliszyk |
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
|
file |
diff |
annotate
|
| 2010-05-05 |
Christian Urban |
solved the problem with equivariance by first eta-normalising the goal
|
file |
diff |
annotate
|
| 2010-05-03 |
Cezary Kaliszyk |
SingleLet and Ex3 work with NewParser.
|
file |
diff |
annotate
|
| 2010-05-03 |
Cezary Kaliszyk |
Equivariance fails for single let?
|
file |
diff |
annotate
|
| 2010-04-20 |
Christian Urban |
renamed Ex1.thy to SingleLet.thy
|
file |
diff |
annotate
| base
|