isabelle-cookbook: ProgTutorial/Appendix.thy@f3536f0b47a9 (annotated)

13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	1
2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	theory Appendix
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	3	imports Base
13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	begin
2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
346 0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	6	(<)
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	7	setup{*
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	8	open_file_with_prelude
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	9	"Recipes_Code.thy"
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	10	["theory Recipes", "imports Main", "begin"]
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	11	*}
0fea8b7a14a1 tuned the ML-output mechanism; tuned slightly the text Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	12	(>)
182 4d0e2edd476d added hyperlinks for every file pointer Christian Urban <urbanc@in.tum.de> parents: 168 diff changeset	13
13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	text {* \appendix *}
2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	15
129 e0d368a45537 started a section about simprocs Christian Urban <urbanc@in.tum.de> parents: 73 diff changeset	16
13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	chapter {* Recipes *}
2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
131 8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 129 diff changeset	19	text {*
184 c7f04a008c9c some polishing Christian Urban <urbanc@in.tum.de> parents: 182 diff changeset	20	Possible topics:
162 3fb9f820a294 some additions to the simplifier section and general tuning Christian Urban <urbanc@in.tum.de> parents: 131 diff changeset	21
168 009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	22	\begin{itemize}
009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	23	\item translations/print translations;
475 25371f74c768 updated to post-2011-1 Isabelle Christian Urban <urbanc@in.tum.de> parents: 407 diff changeset	24	@{ML "Proof_Context.print_syntax"}
131 8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 129 diff changeset	25
168 009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	26	\item user space type systems (in the form that already exists)
164 3f617d7a2691 more work on simple_inductive Christian Urban <urbanc@in.tum.de> parents: 162 diff changeset	27
407 aee4abd02db1 tuned Christian Urban <urbanc@in.tum.de> parents: 356 diff changeset	28	\item useful datastructures: discrimination nets, graphs, association lists
356 43df2d59fb98 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	29
43df2d59fb98 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 346 diff changeset	30	\item Brief history of Isabelle
168 009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	31	\end{itemize}
131 8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 129 diff changeset	32	*}
8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 129 diff changeset	33
168 009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	34	end

author	Christian Urban <urbanc@in.tum.de>
	Sat, 05 Nov 2011 18:44:28 +0000 (2011-11-05)
changeset 485	f3536f0b47a9
parent 475	25371f74c768
child 517	d8c376662bb4
permissions	-rw-r--r--