isabelle: src/HOL/Nominal/Examples/ROOT.ML@2bc882fbe51c (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";
f982e73e36de adjusted for the example file SOS.thy urbanc parents: 22073 diff changeset	18	use_thy "SOS";

author	huffman
	Mon, 28 May 2007 03:45:41 +0200
changeset 23112	2bc882fbe51c
parent 23098	11e1a67fbfe8
child 23144	4a9c9e260abf
permissions	-rw-r--r--