testboard: src/HOL/Nominal/Examples/ROOT.ML@5d8faadf3ecf (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";
23098 11e1a67fbfe8 took out Class.thy from the compiling process until memory problems are solved urbanc parents: 22823 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
	Thu, 31 May 2007 11:00:06 +0200
changeset 23145	5d8faadf3ecf
parent 23144	4a9c9e260abf
child 23158	749b6870b1a1
permissions	-rw-r--r--