isabelle: src/HOL/Nominal/Examples/Nominal_Examples

58329 a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	1	(* Author: Christian Urban TU Muenchen *)
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	2
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 58329 diff changeset	3	section {* Various examples involving nominal datatypes. *}
58329 a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	4
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	5	theory Nominal_Examples_Base
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	6	imports
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	7	CK_Machine
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	8	CR
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	9	CR_Takahashi
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	10	Compile
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	11	Contexts
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	12	Crary
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	13	Fsub
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	14	Height
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	15	Lambda_mu
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	16	LocalWeakening
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	17	Pattern
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	18	SN
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	19	SOS
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	20	Standardization
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	21	Support
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	22	Type_Preservation
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	23	W
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	24	Weakening
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	25	begin
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	26
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	27	end

author	wenzelm
	Sun, 02 Nov 2014 18:21:45 +0100
changeset 58889	5b7a9633cfa8
parent 58329	a31404ec7414
permissions	-rw-r--r--