Nominal/Nominal2_Abs.thy
2011-12-05 Christian Urban tiny improvement by removing one unnecessary assumption
2011-12-05 Christian Urban tuned
2011-09-20 Cezary Kaliszyk minor
2011-09-08 Christian Urban more on paper
2011-07-05 Christian Urban exported various FCB-lemmas to a separate file
2011-06-27 Christian Urban fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction.
2011-06-20 Cezary Kaliszyk Abs_set_fcb
2011-06-20 Cezary Kaliszyk Move lst_fcb to Nominal2_Abs
2011-06-10 Cezary Kaliszyk Slightly modify fcb for list1 and put in common place.
2011-02-28 Christian Urban split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
2011-02-24 Christian Urban added a lemma about fresh_star and Abs
2011-01-31 Cezary Kaliszyk More properties that relate abs_res and abs_set. Also abs_res with less binders.
2011-01-30 Cezary Kaliszyk alpha_res implies alpha_set :)
2011-01-19 Christian Urban ported some of the old proofs to serve as testcases
2011-01-19 Christian Urban added Minimal file to test things
2011-01-18 Christian Urban derived stronger Abs_eq_iff2 theorems
2011-01-18 Christian Urban made alpha_abs_set_stronger1 stronger
2011-01-18 Cezary Kaliszyk alpha_abs_set_stronger1
2011-01-18 Christian Urban the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
2011-01-18 Christian Urban modified the renaming_perm lemmas
2011-01-17 Christian Urban moved high level code from LamTest into the main libraries.
2011-01-14 Christian Urban strengthened renaming lemmas
2011-01-03 Christian Urban simple cases for string rule inductions
2010-12-21 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
2010-12-16 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there
2010-12-07 Christian Urban moved general theorems into the libraries
2010-12-03 Christian Urban updated to Isabelle 2nd December
2010-11-29 Christian Urban isarfied some of the high-level proofs
2010-11-26 Christian Urban completely different method fro deriving the exhaust lemma
2010-11-22 Cezary Kaliszyk current isabelle
less more (0) tip