Nominal/nominal_dt_quot.ML
Wed, 13 Apr 2011 13:41:52 +0100 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
Tue, 04 Jan 2011 13:47:38 +0000 Christian Urban final version of the ESOP paper; used set+ instead of res as requested by one reviewer
Mon, 03 Jan 2011 16:19:27 +0000 Christian Urban simple cases for string rule inductions
Tue, 28 Dec 2010 19:51:25 +0000 Christian Urban automated all strong induction lemmas
less more (0) -10 -4 tip