| author | urbanc |
| Fri, 04 Feb 2011 22:54:29 +0000 | |
| changeset 66 | 828ea293b61f |
| parent 62 | d94209ad2880 |
| permissions | -rw-r--r-- |
|
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}
|
|
62
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
2 |
\usepackage{isabelle}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
3 |
\usepackage{isabellesym}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
4 |
\usepackage{amsmath}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
5 |
\usepackage{amssymb}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
6 |
\usepackage{tikz}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
7 |
\usepackage{pgf}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
8 |
\usepackage{pdfsetup}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
9 |
\usepackage{ot1patch}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
10 |
\usepackage{times}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
11 |
\usepackage{proof}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
12 |
\usepackage{stmaryrd}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
13 |
\usepackage{tikz}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
14 |
\usetikzlibrary{arrows,automata,decorations,fit,calc}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
15 |
\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
16 |
\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
17 |
\usetikzlibrary{matrix}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
18 |
\usepackage{subfigure}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
19 |
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
20 |
\urlstyle{rm}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
21 |
\isabellestyle{it}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
22 |
\renewcommand{\isastyleminor}{\it}%
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
23 |
\renewcommand{\isastyle}{\normalsize\it}%
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
24 |
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
25 |
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
26 |
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
27 |
\renewcommand{\isasymequiv}{$\dn$}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
28 |
\renewcommand{\isasymemptyset}{$\varnothing$}
|
|
d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents:
30
diff
changeset
|
29 |
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
|
|
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
|
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 |
% 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
|
32 |
% 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
|
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 |
%\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
|
35 |
%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
|
36 |
%\<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
|
37 |
%\<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
|
38 |
|
|
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 |
%\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
|
40 |
%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
|
41 |
%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
|
42 |
|
|
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 |
%\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
|
44 |
%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
|
45 |
%\<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
|
46 |
|
|
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 |
%\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
|
48 |
%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
|
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 |
%\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
|
51 |
%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
|
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 |
%\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
|
54 |
%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
|
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 |
% 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
|
57 |
\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
|
58 |
|
|
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 |
% 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
|
60 |
\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
|
61 |
\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
|
62 |
|
|
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 |
% 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
|
64 |
%\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
|
65 |
|
|
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
|
66 |
\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
|
67 |
|
|
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
|
68 |
\title{ListP}
|
|
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
|
69 |
\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
|
70 |
\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
|
71 |
|
|
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
|
72 |
\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
|
73 |
|
|
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
|
74 |
% 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
|
75 |
\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
|
76 |
|
|
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
|
77 |
% 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
|
78 |
\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
|
79 |
|
|
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
|
80 |
% 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
|
81 |
%\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
|
82 |
%\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
|
83 |
|
|
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
|
84 |
\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
|
85 |
|
|
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
|
86 |
%%% 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
|
87 |
%%% 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
|
88 |
%%% 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
|
89 |
%%% End: |