isabelle: src/HOL/Nominal/Examples/ROOT.ML@c33b542394f3 (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";
21086 fe9f43a1e5bd Added Compile and Height examples. berghofe parents: 19499 diff changeset	10	use_thy "Compile";
fe9f43a1e5bd Added Compile and Height examples. berghofe parents: 19499 diff changeset	11	use_thy "Fsub";
fe9f43a1e5bd Added Compile and Height examples. berghofe parents: 19499 diff changeset	12	use_thy "Height";
19499 1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes. berghofe parents: 19495 diff changeset	13	use_thy "Lambda_mu";
1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes. berghofe parents: 19495 diff changeset	14	use_thy "SN";
19495 3d04b87ad8ba New ROOT file for nominal datatype examples. berghofe parents: diff changeset	15	use_thy "Weakening";
22448 f982e73e36de adjusted for the example file SOS.thy urbanc parents: 22073 diff changeset	16	use_thy "Crary";
f982e73e36de adjusted for the example file SOS.thy urbanc parents: 22073 diff changeset	17	use_thy "SOS";

author	urbanc
	Wed, 28 Mar 2007 18:25:23 +0200
changeset 22541	c33b542394f3
parent 22448	f982e73e36de
child 22823	fa9ff469247f
permissions	-rw-r--r--