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

53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	1	theory ToyList_Test
58112 8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place blanchet parents: 57626 diff changeset	2	imports Old_Datatype
53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	3	begin
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	4
57626 2288a6f17930 more official Thy_Info.script_thy; wenzelm parents: 57083 diff changeset	5	ML {*
2288a6f17930 more official Thy_Info.script_thy; wenzelm parents: 57083 diff changeset	6	map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
2288a6f17930 more official Thy_Info.script_thy; wenzelm parents: 57083 diff changeset	7	["ToyList1.txt", "ToyList2.txt"]
2288a6f17930 more official Thy_Info.script_thy; wenzelm parents: 57083 diff changeset	8	\|> implode
2288a6f17930 more official Thy_Info.script_thy; wenzelm parents: 57083 diff changeset	9	\|> Thy_Info.script_thy Position.start
53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	10	*}
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	11
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	12	end