Nominal/Nominal2_Abs.thy
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
2010-11-14 Christian Urban merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
less more (0) tip