src/HOL/Nominal/Examples/ROOT.ML
author berghofe
Fri, 28 Apr 2006 15:55:38 +0200
changeset 19495 3d04b87ad8ba
child 19499 1a082c1257d7
permissions -rw-r--r--
New ROOT file for nominal datatype examples.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19495
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Nominal/Examples/ROOT.ML
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     3
    Author:     Christian Urban, TU Muenchen
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     4
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     5
Various examples involving nominal datatypes.
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     6
*)
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     7
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     8
use_thy "CR";
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     9
use_thy "SN";
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
    10
use_thy "Recursion";
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
    11
use_thy "Weakening";