isabelle-cookbook: ProgTutorial/Appendix.thy@0150cf5982ae (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
2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	imports Main
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
182 4d0e2edd476d added hyperlinks for every file pointer Christian Urban <urbanc@in.tum.de> parents: 168 diff changeset	6
13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	text {* \appendix *}
2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
129 e0d368a45537 started a section about simprocs Christian Urban <urbanc@in.tum.de> parents: 73 diff changeset	9
13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	chapter {* Recipes *}
2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: diff changeset	11
131 8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 129 diff changeset	12	text {*
184 c7f04a008c9c some polishing Christian Urban <urbanc@in.tum.de> parents: 182 diff changeset	13	Possible topics:
162 3fb9f820a294 some additions to the simplifier section and general tuning Christian Urban <urbanc@in.tum.de> parents: 131 diff changeset	14
168 009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	15	\begin{itemize}
009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	16	\item translations/print translations;
162 3fb9f820a294 some additions to the simplifier section and general tuning Christian Urban <urbanc@in.tum.de> parents: 131 diff changeset	17	@{ML "ProofContext.print_syntax"}
131 8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 129 diff changeset	18
168 009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	19	\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	20
184 c7f04a008c9c some polishing Christian Urban <urbanc@in.tum.de> parents: 182 diff changeset	21	\item unification and typing algorithms
c7f04a008c9c some polishing Christian Urban <urbanc@in.tum.de> parents: 182 diff changeset	22	(@{ML_file "Pure/pattern.ML"} implements HOPU)
164 3f617d7a2691 more work on simple_inductive Christian Urban <urbanc@in.tum.de> parents: 162 diff changeset	23
168 009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	24	\item useful datastructures: discrimination nets, association lists
009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	25	\end{itemize}
131 8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 129 diff changeset	26	*}
8db9195bb3e9 polished Christian Urban <urbanc@in.tum.de> parents: 129 diff changeset	27
168 009ca4807baa polished somewhat the recipes and solutions Christian Urban <urbanc@in.tum.de> parents: 164 diff changeset	28	end

author	Christian Urban <urbanc@in.tum.de>
	Thu, 19 Mar 2009 23:21:26 +0100
changeset 191	0150cf5982ae
parent 189	069d525f8f1d
child 346	0fea8b7a14a1
permissions	-rw-r--r--