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

53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	1	theory ToyList_Test
58926 baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined after theory List; wenzelm parents: 58856 diff changeset	2	imports Main
53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	3	begin
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	4
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58926 diff changeset	5	ML \<open>
58856 4fced55fc5b7 provide explicit theory (amending 621c052789b4); wenzelm parents: 58372 diff changeset	6	let val text =
69282 94fa3376ba33 added ML antiquotation @{master_dir}; wenzelm parents: 67406 diff changeset	7	map (File.read o Path.append \<^master_dir>) [\<^path>\<open>ToyList1.txt\<close>, \<^path>\<open>ToyList2.txt\<close>]
58856 4fced55fc5b7 provide explicit theory (amending 621c052789b4); wenzelm parents: 58372 diff changeset	8	\|> implode
58926 baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined after theory List; wenzelm parents: 58856 diff changeset	9	in Thy_Info.script_thy Position.start text @{theory} end
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58926 diff changeset	10	\<close>
53376 1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	11
1d4a46f1fced more robust ToyList_Test; wenzelm parents: diff changeset	12	end

author	wenzelm
	Tue, 27 Nov 2018 23:30:18 +0100
changeset 69351	bff3eb77b0d1
parent 69282	94fa3376ba33
child 69597	ff784d5a5bfb
permissions	-rw-r--r--