isabelle: src/Doc/Tutorial/ToyList/ToyList_Test.thy@902960859c66 (annotated)

53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	1	theory ToyList_Test
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	2	imports Datatype
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	3	begin
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	4
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	5	ML {* (* FIXME somewhat non-standard, fragile *)
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	6	let
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	7	val texts =
56208 06cc31dff138 clarifed module name; wenzelm parents: 53376 diff changeset	8	map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	9	["ToyList1", "ToyList2"];
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	10	val trs = Outer_Syntax.parse Position.start (implode texts);
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	11	val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	12	in @{assert} (Toplevel.is_toplevel end_state) end;
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	13	*}
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	14
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	15	end
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	16

author	wenzelm
	Fri, 11 Apr 2014 19:07:56 +0200
changeset 56546	902960859c66
parent 56208	06cc31dff138
child 57083	5c26000e1042
permissions	-rw-r--r--