isabelle: src/HOL/Nominal/Examples/ROOT.ML@d1dce7d0731c (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",
24895 7cbb842aa99e added two new example files urbanc parents: 24153 diff changeset	21	"Support"
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	22	];
24895 7cbb842aa99e added two new example files urbanc parents: 24153 diff changeset	23
24897 b0a93a6d6ab9 changed file name urbanc parents: 24895 diff changeset	24	setmp quick_and_dirty true use_thy "VC_Compatible";

author	haftmann
	Fri, 23 Nov 2007 21:09:32 +0100
changeset 25459	d1dce7d0731c
parent 24897	b0a93a6d6ab9
child 25722	0a104ddb72d9
permissions	-rw-r--r--