Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated version
authorChristian Urban <urbanc@in.tum.de>
Wed, 28 Jan 2009 06:43:51 +0000
changeset 87 90189a97b3f8
parent 86 fdb9ea86c2a3
child 88 ebbd0dd008c8
updated version
CookBook/FirstSteps.thy file | annotate | diff | comparison | revisions
CookBook/document/implementation.aux file | annotate | diff | comparison | revisions
cookbook.pdf file | annotate | diff | comparison | revisions 
--- a/CookBook/FirstSteps.thy	Wed Jan 28 06:29:16 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 28 06:43:51 2009 +0000
@@ -522,8 +522,8 @@
 
   \begin{readmore}
   The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
-  and @{ML_file "Pure/General/basics.ML"}. The section ?? in the implementation manual
-  contains also information about combinators.
+  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
+  contains further information about combinators.
   \end{readmore}
 
   The simplest combinator is @{ML I}, which is just the identity function.
--- a/CookBook/document/implementation.aux	Wed Jan 28 06:29:16 2009 +0000
+++ b/CookBook/document/implementation.aux	Wed Jan 28 06:43:51 2009 +0000
@@ -13,12 +13,12 @@
 \fi
 
 \providecommand*\HyPL@Entry[1]{}
-\HyPL@Entry{0 << /S /D >> }
-\HyPL@Entry{1 << /S /D >> }
-\HyPL@Entry{2 << /S /D >> }
-\HyPL@Entry{3 << /S /r >> }
+\HyPL@Entry{0<</S/D>>}
+\HyPL@Entry{1<</S/D>>}
+\HyPL@Entry{2<</S/D>>}
+\HyPL@Entry{3<</S/r>>}
 \citation{isabelle-isar-ref}
-\HyPL@Entry{7 << /S /D >> }
+\HyPL@Entry{7<</S/D>>}
 \@writefile{toc}{\contentsline {chapter}{\numberline {1}Preliminaries}{1}{chapter.1}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
@@ -27,7 +27,7 @@
 \newlabel{sec:context-theory}{{1.1.1}{2}{Theory context \label {sec:context-theory}\relax }{subsection.1.1.1}{}}
 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1.1}Theory context }{2}{subsection.1.1.1}}
 \@writefile{lof}{\contentsline {figure}{\numberline {1.1}{\ignorespaces A theory definition depending on ancestors}}{3}{figure.1.1}}
-\newlabel{fig:ex-theory}{{1.1}{3}{Theory context \label {sec:context-theory}\relax }{figure.1.1}{}}
+\newlabel{fig:ex-theory}{{1.1}{3}{A theory definition depending on ancestors\relax }{figure.1.1}{}}
 \newlabel{sec:context-proof}{{1.1.2}{4}{Proof context \label {sec:context-proof}\relax }{subsection.1.1.2}{}}
 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1.2}Proof context }{4}{subsection.1.1.2}}
 \newlabel{sec:generic-context}{{1.1.3}{5}{Generic contexts \label {sec:generic-context}\relax }{subsection.1.1.3}{}}
@@ -65,78 +65,83 @@
 \newlabel{sec:prim-rules}{{2.3.1}{20}{Primitive connectives and rules \label {sec:prim-rules}\relax }{subsection.2.3.1}{}}
 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}Primitive connectives and rules }{20}{subsection.2.3.1}}
 \@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Primitive connectives of Pure}}{20}{figure.2.1}}
-\newlabel{fig:pure-connectives}{{2.1}{20}{Primitive connectives and rules \label {sec:prim-rules}\relax }{figure.2.1}{}}
+\newlabel{fig:pure-connectives}{{2.1}{20}{Primitive connectives of Pure\relax }{figure.2.1}{}}
 \@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces Primitive inferences of Pure}}{21}{figure.2.2}}
-\newlabel{fig:prim-rules}{{2.2}{21}{Primitive connectives and rules \label {sec:prim-rules}\relax }{figure.2.2}{}}
+\newlabel{fig:prim-rules}{{2.2}{21}{Primitive inferences of Pure\relax }{figure.2.2}{}}
 \@writefile{lof}{\contentsline {figure}{\numberline {2.3}{\ignorespaces Conceptual axiomatization of Pure equality}}{21}{figure.2.3}}
-\newlabel{fig:pure-equality}{{2.3}{21}{Primitive connectives and rules \label {sec:prim-rules}\relax }{figure.2.3}{}}
+\newlabel{fig:pure-equality}{{2.3}{21}{Conceptual axiomatization of Pure equality\relax }{figure.2.3}{}}
 \@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces Admissible substitution rules}}{21}{figure.2.4}}
-\newlabel{fig:subst-rules}{{2.4}{21}{Primitive connectives and rules \label {sec:prim-rules}\relax }{figure.2.4}{}}
+\newlabel{fig:subst-rules}{{2.4}{21}{Admissible substitution rules\relax }{figure.2.4}{}}
 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}Auxiliary definitions}{24}{subsection.2.3.2}}
 \@writefile{lof}{\contentsline {figure}{\numberline {2.5}{\ignorespaces Definitions of auxiliary connectives}}{24}{figure.2.5}}
-\newlabel{fig:pure-aux}{{2.5}{24}{Auxiliary definitions\relax }{figure.2.5}{}}
-\newlabel{sec:rules}{{2.4}{25}{Rules \label {sec:rules}\relax }{section.2.4}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {2.4}Rules }{25}{section.2.4}}
+\newlabel{fig:pure-aux}{{2.5}{24}{Definitions of auxiliary connectives\relax }{figure.2.5}{}}
+\newlabel{sec:obj-rules}{{2.4}{25}{Object-level rules \label {sec:obj-rules}\relax }{section.2.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {2.4}Object-level rules }{25}{section.2.4}}
 \@writefile{toc}{\contentsline {chapter}{\numberline {3}Tactical reasoning}{26}{chapter.3}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
 \newlabel{sec:tactical-goals}{{3.1}{26}{Goals \label {sec:tactical-goals}\relax }{section.3.1}{}}
 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Goals }{26}{section.3.1}}
 \@writefile{toc}{\contentsline {section}{\numberline {3.2}Tactics}{27}{section.3.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {3.3}Tacticals}{27}{section.3.3}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {4}Structured proofs}{28}{chapter.4}}
+\newlabel{sec:resolve-assume-tac}{{3.2.1}{29}{Resolution and assumption tactics \label {sec:resolve-assume-tac}\relax }{subsection.3.2.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Resolution and assumption tactics }{29}{subsection.3.2.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.2}Explicit instantiation within a subgoal context}{31}{subsection.3.2.2}}
+\newlabel{sec:tacticals}{{3.3}{32}{Tacticals \label {sec:tacticals}\relax }{section.3.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.3}Tacticals }{32}{section.3.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {4}Structured proofs}{33}{chapter.4}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\newlabel{sec:variables}{{4.1}{28}{Variables \label {sec:variables}\relax }{section.4.1}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {4.1}Variables }{28}{section.4.1}}
-\newlabel{sec:assumptions}{{4.2}{30}{Assumptions \label {sec:assumptions}\relax }{section.4.2}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {4.2}Assumptions }{30}{section.4.2}}
+\newlabel{sec:variables}{{4.1}{33}{Variables \label {sec:variables}\relax }{section.4.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.1}Variables }{33}{section.4.1}}
+\newlabel{sec:assumptions}{{4.2}{35}{Assumptions \label {sec:assumptions}\relax }{section.4.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.2}Assumptions }{35}{section.4.2}}
 \citation{isabelle-isar-ref}
-\newlabel{sec:results}{{4.3}{32}{Results \label {sec:results}\relax }{section.4.3}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {4.3}Results }{32}{section.4.3}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {5}Isar proof texts}{34}{chapter.5}}
+\newlabel{sec:results}{{4.3}{37}{Results \label {sec:results}\relax }{section.4.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.3}Results }{37}{section.4.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {5}Isar proof texts}{39}{chapter.5}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {5.1}Proof context}{34}{section.5.1}}
-\newlabel{sec:isar-proof-state}{{5.2}{34}{Proof state \label {sec:isar-proof-state}\relax }{section.5.2}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {5.2}Proof state }{34}{section.5.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {5.3}Proof methods}{34}{section.5.3}}
-\@writefile{toc}{\contentsline {section}{\numberline {5.4}Attributes}{34}{section.5.4}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {6}Structured specifications}{35}{chapter.6}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.1}Proof context}{39}{section.5.1}}
+\newlabel{sec:isar-proof-state}{{5.2}{39}{Proof state \label {sec:isar-proof-state}\relax }{section.5.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.2}Proof state }{39}{section.5.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.3}Proof methods}{39}{section.5.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.4}Attributes}{39}{section.5.4}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {6}Structured specifications}{40}{chapter.6}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {6.1}Specification elements}{35}{section.6.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.2}Type-inference}{35}{section.6.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.3}Local theories}{35}{section.6.3}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {7}System integration}{36}{chapter.7}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.1}Specification elements}{40}{section.6.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.2}Type-inference}{40}{section.6.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.3}Local theories}{40}{section.6.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {7}System integration}{41}{chapter.7}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\newlabel{sec:isar-toplevel}{{7.1}{36}{Isar toplevel \label {sec:isar-toplevel}\relax }{section.7.1}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.1}Isar toplevel }{36}{section.7.1}}
-\newlabel{sec:toplevel-transition}{{7.1.1}{37}{Toplevel transitions \label {sec:toplevel-transition}\relax }{subsection.7.1.1}{}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Toplevel transitions }{37}{subsection.7.1.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Toplevel control}{39}{subsection.7.1.2}}
-\newlabel{sec:ML-toplevel}{{7.2}{39}{ML toplevel \label {sec:ML-toplevel}\relax }{section.7.2}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.2}ML toplevel }{39}{section.7.2}}
-\newlabel{sec:theory-database}{{7.3}{41}{Theory database \label {sec:theory-database}\relax }{section.7.3}{}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.3}Theory database }{41}{section.7.3}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {A}Advanced ML programming}{44}{appendix.A}}
+\newlabel{sec:isar-toplevel}{{7.1}{41}{Isar toplevel \label {sec:isar-toplevel}\relax }{section.7.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.1}Isar toplevel }{41}{section.7.1}}
+\newlabel{sec:toplevel-transition}{{7.1.1}{42}{Toplevel transitions \label {sec:toplevel-transition}\relax }{subsection.7.1.1}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Toplevel transitions }{42}{subsection.7.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Toplevel control}{44}{subsection.7.1.2}}
+\newlabel{sec:ML-toplevel}{{7.2}{44}{ML toplevel \label {sec:ML-toplevel}\relax }{section.7.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.2}ML toplevel }{44}{section.7.2}}
+\newlabel{sec:theory-database}{{7.3}{46}{Theory database \label {sec:theory-database}\relax }{section.7.3}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.3}Theory database }{46}{section.7.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {A}Advanced ML programming}{49}{appendix.A}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {A.1}Style}{44}{section.A.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {A.2}Thread-safe programming}{45}{section.A.2}}
-\@writefile{toc}{\contentsline {paragraph}{Critical shared resources.}{46}{section*.26}}
-\@writefile{toc}{\contentsline {paragraph}{Multithreading in Isabelle/Isar.}{46}{section*.27}}
-\@writefile{toc}{\contentsline {paragraph}{Good conduct of impure programs.}{47}{section*.28}}
-\@writefile{toc}{\contentsline {chapter}{\numberline {B}Basic library functions}{49}{appendix.B}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.1}Style}{49}{section.A.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {A.2}Thread-safe programming}{50}{section.A.2}}
+\@writefile{toc}{\contentsline {paragraph}{Critical shared resources.}{51}{section*.29}}
+\@writefile{toc}{\contentsline {paragraph}{Multithreading in Isabelle/Isar.}{51}{section*.30}}
+\@writefile{toc}{\contentsline {paragraph}{Good conduct of impure programs.}{52}{section*.31}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {B}Basic library functions}{54}{appendix.B}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {B.1}Linear transformations}{49}{section.B.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {B.2}Options and partiality}{52}{section.B.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {B.3}Common data structures}{52}{section.B.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.1}Lists (as set-like data structures)}{52}{subsection.B.3.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.2}Association lists}{53}{subsection.B.3.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.3}Tables}{54}{subsection.B.3.3}}
+\newlabel{sec:ML-linear-trans}{{B.1}{54}{Linear transformations \label {sec:ML-linear-trans}\relax }{section.B.1}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {B.1}Linear transformations }{54}{section.B.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {B.2}Options and partiality}{57}{section.B.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {B.3}Common data structures}{57}{section.B.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.1}Lists (as set-like data structures)}{57}{subsection.B.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.2}Association lists}{58}{subsection.B.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.3.3}Tables}{59}{subsection.B.3.3}}
 \bibstyle{plain}
 \bibdata{../manual}
 \bibcite{Barendregt-Geuvers:2001}{1}
@@ -146,5 +151,5 @@
 \bibcite{paulson700}{5}
 \bibcite{paulson-ml2}{6}
 \bibcite{isabelle-isar-ref}{7}
-\@writefile{toc}{\contentsline {chapter}{Bibliography}{55}{section*.36}}
-\@writefile{toc}{\contentsline {chapter}{Index}{56}{section*.38}}
+\@writefile{toc}{\contentsline {chapter}{Bibliography}{60}{section*.39}}
+\@writefile{toc}{\contentsline {chapter}{Index}{61}{section*.41}}
Binary file cookbook.pdf has changed
isabelle-cookbook