isabelle: src/HOL/Nominal/Examples/ROOT.ML@51a18dd1ea86 (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";
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 21136 diff changeset	16	use_thy "Crary";

author	narboux
	Tue, 06 Mar 2007 16:40:32 +0100
changeset 22421	51a18dd1ea86
parent 22073	c170dcbe6c9d
child 22448	f982e73e36de
permissions	-rw-r--r--