2011-06-29 Christian Urban combined distributed data for alpha in alpha_result (partially done)
2011-06-29 Christian Urban moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
2011-06-29 Christian Urban added a warning if a theorem is already declared as equivariant
2011-06-29 Christian Urban merged
2011-06-29 Cezary Kaliszyk Prove bn injectivity and experiment more with Let
2011-06-28 Christian Urban some experiments
2011-06-28 Cezary Kaliszyk trying new fcb in let/subst
2011-06-28 Cezary Kaliszyk Leftover only inj and eqvt
2011-06-28 Cezary Kaliszyk eapply fcb ok
2011-06-28 Cezary Kaliszyk Removed Inl and Inr
2011-06-28 Christian Urban relaxed type in fcb
2011-06-28 Christian Urban fcb with explicit bn function
2011-06-28 Christian Urban added let-rec example
2011-06-28 Cezary Kaliszyk Experiments with res
2011-06-27 Christian Urban proved the fcb also for sets (no restriction yet)
2011-06-27 Christian Urban copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom
(0) -1000 -300 -100 -16 +16 +100 +300 tip