src/HOL/Nominal/Examples/Crary.thy
Mon, 14 Apr 2008 21:44:53 +0200 wenzelm avoid duplicate fact bindings;
Fri, 19 Oct 2007 23:21:08 +0200 wenzelm tuned proofs: avoid implicit prems;
Sun, 12 Aug 2007 18:53:03 +0200 wenzelm added type constraints to resolve syntax ambiguities;
Tue, 31 Jul 2007 14:45:36 +0200 narboux undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
Mon, 30 Jul 2007 10:39:12 +0200 urbanc updated some of the definitions and proofs
Wed, 11 Jul 2007 11:36:06 +0200 berghofe Renamed inductive2 to inductive.
less more (0) -10 -6 tip