isabelle: src/HOL/Nominal/Examples/Nominal_Examples.thy@9be4ab2acc13 (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
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	7	CR
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	8	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	9	Class3
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	10	Compile
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	11	Fsub
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	12	Height
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	13	Lambda_mu
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	14	SN
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	15	Weakening
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	16	Crary
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	17	SOS
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	18	LocalWeakening
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	19	Support
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	20	Contexts
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	21	Standardization
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	22	W
33189 82a40677c1f8 Added Pattern.thy to Nominal/Examples. berghofe parents: 32635 diff changeset	23	Pattern
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	24	begin
24895 7cbb842aa99e added two new example files urbanc parents: 24153 diff changeset	25
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	26	end

author	wenzelm
	Thu, 22 Apr 2010 22:01:06 +0200
changeset 36277	9be4ab2acc13
parent 33189	82a40677c1f8
child 37358	74fb4f03bb51
permissions	-rw-r--r--