isabelle: src/Doc/Tutorial/ToyList/ToyList_Test.thy@608c157d743d (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 =
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	8	map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
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	paulson <lp15@cam.ac.uk>
	Wed, 29 Jan 2014 12:51:37 +0000
changeset 55159	608c157d743d
parent 53376	1d4a46f1fced
child 56208	06cc31dff138
permissions	-rw-r--r--