isabelle: src/Doc/Tutorial/ToyList/ToyList_Test.thy@f0f623005324 (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 {*
58856 4fced55fc5b7 provide explicit theory (amending 621c052789b4); wenzelm parents: 58372 diff changeset	6	let val text =
4fced55fc5b7 provide explicit theory (amending 621c052789b4); wenzelm parents: 58372 diff changeset	7	map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
4fced55fc5b7 provide explicit theory (amending 621c052789b4); wenzelm parents: 58372 diff changeset	8	["ToyList1.txt", "ToyList2.txt"]
4fced55fc5b7 provide explicit theory (amending 621c052789b4); wenzelm parents: 58372 diff changeset	9	\|> implode
4fced55fc5b7 provide explicit theory (amending 621c052789b4); wenzelm parents: 58372 diff changeset	10	in Thy_Info.script_thy Position.start text @{theory BNF_Least_Fixpoint} end
53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	11	*}
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	12
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	13	end

author	wenzelm
	Sun, 02 Nov 2014 16:47:45 +0100
changeset 58872	f0f623005324
parent 58856	4fced55fc5b7
child 58926	baf5a3c28f0c
permissions	-rw-r--r--