isabelle: src/HOL/Nominal/Examples/ROOT.ML@34f7b0fbe047 (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",
27623 8e9c19529a4e Added Standardization theory. berghofe parents: 25722 diff changeset	22	"Contexts",
28654 2f9857126498 Added theory W. berghofe parents: 28392 diff changeset	23	"Standardization",
2f9857126498 Added theory W. berghofe parents: 28392 diff changeset	24	"W"
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 23371 diff changeset	25	];
24895 7cbb842aa99e added two new example files urbanc parents: 24153 diff changeset	26
28392 d10839c203bd setmp_noncritical; wenzelm parents: 27623 diff changeset	27	setmp_noncritical quick_and_dirty true use_thy "VC_Condition";

author	wenzelm
	Fri, 24 Jul 2009 20:55:56 +0200
changeset 32173	34f7b0fbe047
parent 28654	2f9857126498
child 32635	37e32f8aa696
permissions	-rw-r--r--