nominal2: Nominal/Ex/Term8.thy@c39d4fe31100 (annotated)

2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Term8
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	imports "../NewParser"
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2045 diff changeset	5	(* example 8 *)
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	atom_decl name
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2045 diff changeset	9	(* this should work but gives an error at the moment:
2097 60ce41a11180 Term8 comment Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2082 diff changeset	10	in alpha_bn_rsp proof.
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2045 diff changeset	11	*)
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2045 diff changeset	12
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	nominal_datatype foo =
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	Foo0 "name"
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	\| Foo1 b::"bar" f::"foo" bind_set "bv b" in f
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	and bar =
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	Bar0 "name"
2097 60ce41a11180 Term8 comment Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2082 diff changeset	18	\| Bar1 "name" s::"name" b::"bar" bind_set s in b
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	binder
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	bv
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	where
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	"bv (Bar0 x) = {}"
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	\| "bv (Bar1 v x b) = {atom v}"
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2045 diff changeset	25
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	end
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28

author	Christian Urban <urbanc@in.tum.de>
	Sun, 16 May 2010 12:41:27 +0100 (2010-05-16)
changeset 2142	c39d4fe31100
parent 2097	60ce41a11180
child 2147	e83493622e6f
permissions	-rw-r--r--