Nominal/Ex/SingleLet.thy
2010-06-23 Christian Urban merged cezary's changes
2010-06-23 Cezary Kaliszyk Un-do the second change to SingleLet.
2010-06-23 Cezary Kaliszyk merge
2010-06-23 Cezary Kaliszyk Changes for PER and list_all2 committed to Isabelle
2010-06-22 Christian Urban proved eqvip theorems for alphas
2010-06-22 Christian Urban prove that alpha implies alpha_bn (needed for rsp proofs)
2010-06-21 Christian Urban merged with main line
2010-06-11 Christian Urban also symmetry
2010-06-09 Christian Urban transitivity proofs done
2010-06-07 Christian Urban merged
2010-06-07 Christian Urban work on transitivity proof
2010-06-02 Christian Urban fixed problem with bn_info
2010-06-01 Christian Urban equivariance done
2010-06-01 Christian Urban smaller code for raw-eqvt proofs
2010-05-31 Christian Urban all raw definitions are defined using function
2010-05-27 Christian Urban merged
2010-05-27 Christian Urban intermediate state
2010-05-24 Christian Urban added slides
2010-05-24 Christian Urban alpha works now
2010-05-23 Christian Urban started to work on alpha
2010-05-22 Christian Urban properly exported bn_descr
2010-05-21 Christian Urban hving a working fv-definition without the export
2010-05-21 Christian Urban tuned
2010-05-20 Christian Urban new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
2010-06-20 Christian Urban fixed example
2010-06-07 Christian Urban improved abstract, some tuning
2010-05-27 Christian Urban fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
2010-05-17 Christian Urban minor tuning
2010-05-12 Christian Urban fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
2010-05-12 Christian Urban moved the data-transformation into the parser
less more (0) -30 tip