regexp: tphols-2011/generated/root.tex@f5db9e08effc (annotated)

30 f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	1	\documentclass[11pt,a4paper]{article}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	2	\usepackage{isabelle,isabellesym}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	3	\usepackage{amsmath}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	4	%\usepackage[pdftex]{hyperref}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	5
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	6	% further packages required for unusual symbols (see also
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	7	% isabellesym.sty), use only when needed
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	8
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	9	%\usepackage{amssymb}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	10	%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	11	%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	12	%\<triangleq>, \<yen>, \<lozenge>
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	13
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	14	%\usepackage[greek,english]{babel}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	15	%option greek for \<euro>
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	16	%option english (default language) for \<guillemotleft>, \<guillemotright>
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	17
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	18	%\usepackage[latin1]{inputenc}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	19	%for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	20	%\<threesuperior>, \<threequarters>, \<degree>
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	21
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	22	%\usepackage[only,bigsqcap]{stmaryrd}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	23	%for \<Sqinter>
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	24
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	25	%\usepackage{eufrak}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	26	%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	27
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	28	%\usepackage{textcomp}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	29	%for \<cent>, \<currency>
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	30
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	31	% this should be the last package used
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	32	\usepackage{pdfsetup}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	33
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	34	% urls in roman style, theory text in math-similar italics
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	35	\urlstyle{rm}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	36	\isabellestyle{it}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	37
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	38	% for uniform font size
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	39	%\renewcommand{\isastyle}{\isastyleminor}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	40
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	41
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	42	\begin{document}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	43
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	44	\title{tphols-2011}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	45	\author{By xingyuan}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	46	\maketitle
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	47
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	48	\tableofcontents
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	49
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	50	% sane default for proof documents
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	51	\parindent 0pt\parskip 0.5ex
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	52
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	53	% generated text of all theories
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	54	\input{session}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	55
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	56	% optional bibliography
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	57	%\bibliographystyle{abbrv}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	58	%\bibliography{root}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	59
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	60	\end{document}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	61
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	62	%%% Local Variables:
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	63	%%% mode: latex
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	64	%%% TeX-master: t
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: diff changeset	65	%%% End:

author	zhang
	Mon, 24 Jan 2011 11:29:55 +0000
changeset 30	f5db9e08effc
permissions	-rw-r--r--