isabelle: src/HOL/Nominal/Examples/Nominal_Examples.thy@22f665a2e91c (annotated)

32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	1	(* Author: Christian Urban TU Muenchen *)
19495 3d04b87ad8ba New ROOT file for nominal datatype examples. berghofe parents: diff changeset	2
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	3	header {* Various examples involving nominal datatypes. *}
19495 3d04b87ad8ba New ROOT file for nominal datatype examples. berghofe parents: diff changeset	4
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	5	theory Nominal_Examples
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	6	imports
37358 74fb4f03bb51 recovered some untested theories; wenzelm parents: 36277 diff changeset	7	CK_Machine
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	8	CR
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	9	CR_Takahashi
36277 9be4ab2acc13 split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available; wenzelm parents: 33189 diff changeset	10	Class3
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	11	Compile
37358 74fb4f03bb51 recovered some untested theories; wenzelm parents: 36277 diff changeset	12	Contexts
74fb4f03bb51 recovered some untested theories; wenzelm parents: 36277 diff changeset	13	Crary
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	14	Fsub
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	15	Height
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	16	Lambda_mu
37358 74fb4f03bb51 recovered some untested theories; wenzelm parents: 36277 diff changeset	17	LocalWeakening
74fb4f03bb51 recovered some untested theories; wenzelm parents: 36277 diff changeset	18	Pattern
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	19	SN
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	20	SOS
37358 74fb4f03bb51 recovered some untested theories; wenzelm parents: 36277 diff changeset	21	Standardization
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	22	Support
37358 74fb4f03bb51 recovered some untested theories; wenzelm parents: 36277 diff changeset	23	Type_Preservation
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	24	W
37358 74fb4f03bb51 recovered some untested theories; wenzelm parents: 36277 diff changeset	25	Weakening
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	26	begin
24895 7cbb842aa99e added two new example files urbanc parents: 24153 diff changeset	27
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	28	end

author	nipkow
	Mon, 12 Sep 2011 07:55:43 +0200
changeset 44890	22f665a2e91c
parent 37358	74fb4f03bb51
child 58329	a31404ec7414
permissions	-rw-r--r--