nominal2: Nominal/Ex/Lambda.thy@a9a1ed3f5023 (annotated)

1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	1	theory Lambda
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2442 diff changeset	2	imports "../Nominal2"
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	7	nominal_datatype lam =
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	8	Var "name"
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	9	\| App "lam" "lam"
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	10	\| Lam x::"name" l::"lam" bind x in l
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	11
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	12	thm lam.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	13	thm lam.induct
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2559 diff changeset	14	thm lam.exhaust lam.strong_exhaust
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	15	thm lam.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	16	thm lam.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	17	thm lam.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	18	thm lam.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	19	thm lam.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	20	thm lam.size_eqvt
2431 331873ebc5cd can now deal with type variables in nominal datatype definitions Christian Urban <urbanc@in.tum.de> parents: 2425 diff changeset	21
2654 0f0335d91456 solved subgoals for depth and subst function Christian Urban <urbanc@in.tum.de> parents: 2649 diff changeset	22
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	end
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26

author	Christian Urban <urbanc@in.tum.de>
	Mon, 17 Jan 2011 12:37:37 +0000
changeset 2664	a9a1ed3f5023
parent 2654	0f0335d91456
child 2666	324a5d1289a3
permissions	-rw-r--r--