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

53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	1	theory ToyList_Test
58372 bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) blanchet parents: 58112 diff changeset	2	imports BNF_Least_Fixpoint
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