author | berghofe |
Fri, 28 Apr 2006 15:55:38 +0200 | |
changeset 19495 | 3d04b87ad8ba |
parent 19494 | 2e909d5309f4 |
child 19496 | 79dbe35c6cba |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nominal/Examples/ROOT.ML Fri Apr 28 15:55:38 2006 +0200 @@ -0,0 +1,11 @@ +(* Title: HOL/Nominal/Examples/ROOT.ML + ID: $Id$ + Author: Christian Urban, TU Muenchen + +Various examples involving nominal datatypes. +*) + +use_thy "CR"; +use_thy "SN"; +use_thy "Recursion"; +use_thy "Weakening";