isabelle: src/HOL/Nominal/Examples/ROOT.ML@ccd9cb15c062 (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";
22823 fa9ff469247f tuned some proofs in CR and properly included CR_Takahashi urbanc parents: 22448 diff changeset	9	use_thy "CR_Takahashi";
23371 ed60e560048d reactivated theory Class; wenzelm parents: 23283 diff changeset	10	use_thy "Class";
21086 fe9f43a1e5bd Added Compile and Height examples. berghofe parents: 19499 diff changeset	11	use_thy "Compile";
fe9f43a1e5bd Added Compile and Height examples. berghofe parents: 19499 diff changeset	12	use_thy "Fsub";
fe9f43a1e5bd Added Compile and Height examples. berghofe parents: 19499 diff changeset	13	use_thy "Height";
19499 1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes. berghofe parents: 19495 diff changeset	14	use_thy "Lambda_mu";
1a082c1257d7 Added Class, Fsub, and Lambda_mu examples for nominal datatypes. berghofe parents: 19495 diff changeset	15	use_thy "SN";
19495 3d04b87ad8ba New ROOT file for nominal datatype examples. berghofe parents: diff changeset	16	use_thy "Weakening";
22448 f982e73e36de adjusted for the example file SOS.thy urbanc parents: 22073 diff changeset	17	use_thy "Crary";
23144 4a9c9e260abf included new example in the compiling process urbanc parents: 23098 diff changeset	18	use_thy "SOS";
23145 5d8faadf3ecf fixed use_thy "LocalWeakening"; wenzelm parents: 23144 diff changeset	19	use_thy "LocalWeakening";

author	wenzelm
	Tue, 10 Jul 2007 23:29:43 +0200
changeset 23719	ccd9cb15c062
parent 23371	ed60e560048d
child 24153	1a4607b7ad24
permissions	-rw-r--r--