nominal2: Nominal/Ex/Test.thy@871d8a5e0c67 (annotated)

954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Test
2062 65bdcc42badd "isabelle make" compiles all examples with newparser/newfv/newalpha only. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2045 diff changeset	2	imports "../NewParser"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1599 diff changeset	5	(* This file contains only the examples that are not supposed to work yet. *)
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1599 diff changeset	6
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1599 diff changeset	7
2143 871d8a5e0c67 somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms Christian Urban <urbanc@in.tum.de> parents: 2103 diff changeset	8	declare [[STEPS = 2]]
871d8a5e0c67 somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms Christian Urban <urbanc@in.tum.de> parents: 2103 diff changeset	9
1428 4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	10	atom_decl name
4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	11
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	12	(* example 4 from Terms.thy *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	13	(* fv_eqvt does not work, we need to repaire defined permute functions
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	14	defined fv and defined alpha... *)
2103 e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	15	(* lists-datastructure does not work yet *)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	16
2103 e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	17	nominal_datatype trm =
e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	18	Vr "name"
e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	19	\| Ap "trm" "trm list"
e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	20	\| Lm x::"name" t::"trm" bind x in t
2143 871d8a5e0c67 somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms Christian Urban <urbanc@in.tum.de> parents: 2103 diff changeset	21
2103 e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	22
e08e3c29dbc0 a bit for the introduction of the q-paper Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	23	(*
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	24	thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	25	thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	26	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	27
961 0f88e04eb486 Variable takes a 'name'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 954 diff changeset	28	end
1223 160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	29
160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	30

author	Christian Urban <urbanc@in.tum.de>
	Mon, 17 May 2010 12:00:54 +0100 (2010-05-17)
changeset 2143	871d8a5e0c67
parent 2103	e08e3c29dbc0
child 2163	5dc48e1af733
permissions	-rw-r--r--