isabelle: src/HOL/Nominal/Examples/Nominal_Examples.thy@37e32f8aa696 (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
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	9	Class
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
37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	23	begin
24895 7cbb842aa99e added two new example files urbanc parents: 24153 diff changeset	24
32635 37e32f8aa696 added session theory for Nominal_Examples haftmann parents: 28654 diff changeset	25	end

author	haftmann
	Mon, 21 Sep 2009 16:01:30 +0200
changeset 32635	37e32f8aa696
parent 28654	src/HOL/Nominal/Examples/ROOT.ML@2f9857126498
child 33189	82a40677c1f8
permissions	-rw-r--r--