isabelle: src/HOL/Nominal/Examples/ROOT.ML@a2fb9d553aad (annotated)

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";
19499 1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes. berghofe parents: 19495 diff changeset	9	use_thy "Class";
1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes. berghofe parents: 19495 diff changeset	10	setmp quick_and_dirty true use_thy "Fsub"; (* FIXME *)
1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes. berghofe parents: 19495 diff changeset	11	use_thy "Lambda_mu";
19495 3d04b87ad8ba New ROOT file for nominal datatype examples. berghofe parents: diff changeset	12	use_thy "Recursion";
19499 1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes. berghofe parents: 19495 diff changeset	13	use_thy "SN";
19495 3d04b87ad8ba New ROOT file for nominal datatype examples. berghofe parents: diff changeset	14	use_thy "Weakening";

author	wenzelm
	Sat, 08 Jul 2006 12:54:38 +0200
changeset 20050	a2fb9d553aad
parent 19499	1a082c1257d7
child 21086	fe9f43a1e5bd
permissions	-rw-r--r--