src/HOL/Nominal/Examples/Height.thy
Wed, 18 Oct 2006 23:15:16 +0200 urbanc cleaning up
Fri, 18 Aug 2006 18:46:02 +0200 urbanc modified to use the characteristic equations
Thu, 17 Aug 2006 20:31:36 +0200 urbanc used the recursion combinator for the height and substitution function
Thu, 01 Jun 2006 14:40:22 +0200 urbanc added an example suggested by D. Wang on the PoplMark-mailing list;
less more (0) tip