isabelle: src/HOL/Nominal/Examples/ROOT.ML@b5b8afc9fdcd (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
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	8	use_thys [
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	9	"CR",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	10	"CR_Takahashi",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	11	"Class",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	12	"Compile",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	13	"Fsub",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	14	"Height",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	15	"Lambda_mu",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	16	"SN",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	17	"Weakening",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	18	"Crary",
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	19	"SOS",
24897 b0a93a6d6ab9 changed file name urbanc parents: 24895 diff changeset	20	"LocalWeakening",
25722 0a104ddb72d9 polishing of some proofs urbanc parents: 24897 diff changeset	21	"Support",
0a104ddb72d9 polishing of some proofs urbanc parents: 24897 diff changeset	22	"Contexts"
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	23	];
24895 7cbb842aa99e added two new example files urbanc parents: 24153 diff changeset	24
25722 0a104ddb72d9 polishing of some proofs urbanc parents: 24897 diff changeset	25	setmp quick_and_dirty true use_thy "VC_Condition";

author	wenzelm
	Thu, 29 May 2008 23:46:41 +0200
changeset 27020	b5b8afc9fdcd
parent 25722	0a104ddb72d9
child 27623	8e9c19529a4e
permissions	-rw-r--r--