Quot/Nominal/Abs.thy
Wed, 24 Feb 2010 18:38:49 +0100 Cezary Kaliszyk Simplified and finised eqvt proofs for t1 and t5
Mon, 22 Feb 2010 15:03:48 +0100 Cezary Kaliszyk Generalize atom_trans and atom_sym.
Thu, 18 Feb 2010 23:07:28 +0100 Christian Urban start work with the parser
Fri, 12 Feb 2010 16:04:10 +0100 Cezary Kaliszyk renamed 'as' to 'is' everywhere.
Thu, 11 Feb 2010 10:06:02 +0100 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2.
Tue, 09 Feb 2010 15:20:52 +0100 Christian Urban merged
Tue, 09 Feb 2010 15:20:40 +0100 Christian Urban a few more attempts to show the equivalence between old and new way of defining alpha-equivalence
Tue, 09 Feb 2010 10:48:42 +0100 Cezary Kaliszyk Fixed pattern matching, now the test in Abs works correctly.
Mon, 08 Feb 2010 13:50:52 +0100 Christian Urban added a test case
Mon, 08 Feb 2010 13:12:55 +0100 Christian Urban moved some lemmas to Nominal; updated all files
Thu, 04 Feb 2010 17:39:04 +0100 Christian Urban fixed (permute_eqvt in eqvts makes this simpset always looping)
Wed, 03 Feb 2010 12:31:58 +0100 Christian Urban fixed proofs in Abs.thy
Wed, 03 Feb 2010 11:21:34 +0100 Cezary Kaliszyk Minor
Tue, 02 Feb 2010 12:48:12 +0100 Cezary Kaliszyk Disambiguating the syntax.
less more (0) -14 tip