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
a31404ec7414 run larger nominal examples only 'ISABELLE_FULL_TEST' blanchet parents: diff changeset	3	header {* Various examples involving nominal datatypes. *}
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	blanchet
	Fri, 12 Sep 2014 16:42:36 +0200
changeset 58329	a31404ec7414
child 58889	5b7a9633cfa8
permissions	-rw-r--r--