*** empty log message ***
authornipkow
Tue Mar 13 18:35:48 2001 +0100 (2001-03-13)
changeset 11203881222d48777
parent 11202 f8da11ca4c6e
child 11204 bb01189f0565
*** empty log message ***
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/ROOT.ML
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/todo.tobias
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Mon Mar 12 18:23:11 2001 +0100
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Tue Mar 13 18:35:48 2001 +0100
     1.3 @@ -164,7 +164,7 @@
     1.4  
     1.5  $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
     1.6    Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
     1.7 -  Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
     1.8 +  Misc/types.thy Misc/prime_def.thy Misc/Translations.thy Misc/case_exprs.thy \
     1.9    Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
    1.10  	$(USEDIR) Misc
    1.11  	@rm -f tutorial.dvi
     2.1 --- a/doc-src/TutorialI/Misc/ROOT.ML	Mon Mar 12 18:23:11 2001 +0100
     2.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML	Tue Mar 13 18:35:48 2001 +0100
     2.3 @@ -8,6 +8,7 @@
     2.4  use_thy "Option2";
     2.5  use_thy "types";
     2.6  use_thy "prime_def";
     2.7 +use_thy "Translations";
     2.8  use_thy "simp";
     2.9  use_thy "Itrev";
    2.10  use_thy "AdvancedInd";
     3.1 --- a/doc-src/TutorialI/Sets/sets.tex	Mon Mar 12 18:23:11 2001 +0100
     3.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Tue Mar 13 18:35:48 2001 +0100
     3.3 @@ -323,18 +323,17 @@
     3.4  \rulename{UN_E}
     3.5  \end{isabelle}
     3.6  %
     3.7 -The following built-in abbreviation lets us express the union
     3.8 -over a \emph{type}:
     3.9 +The following built-in syntax translation (see \S\ref{sec:def-translations})
    3.10 +lets us express the union over a \emph{type}:
    3.11  \begin{isabelle}
    3.12  \ \ \ \ \
    3.13  ({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
    3.14  ({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
    3.15  \end{isabelle}
    3.16 -Abbreviations work as you might expect.  The term on the left-hand side of
    3.17 -the
    3.18 -\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} symbol is automatically translated to the right-hand side when the
    3.19 -term is parsed, the reverse translation being done when the term is
    3.20 -displayed.
    3.21 +%Abbreviations work as you might expect.  The term on the left-hand side of
    3.22 +%the \isasymrightleftharpoons\ symbol is automatically translated to the right-hand side when the
    3.23 +%term is parsed, the reverse translation being done when the term is
    3.24 +%displayed.
    3.25  
    3.26  We may also express the union of a set of sets, written \isa{Union\ C} in
    3.27  \textsc{ascii}: 
    3.28 @@ -426,10 +425,10 @@
    3.29  $\binom{n}{k}$.
    3.30  
    3.31  \begin{warn}
    3.32 -The term \isa{Finite\ A} is an abbreviation for
    3.33 -\isa{A\ \isasymin\ Finites}, where the constant \isa{Finites} denotes the
    3.34 -set of all finite sets of a given type.  There is no constant
    3.35 -\isa{Finite}.
    3.36 +The term \isa{finite\ A} is defined via a syntax translation as an
    3.37 +abbreviation for \isa{A \isasymin Finites}, where the constant \isa{Finites}
    3.38 +denotes the set of all finite sets of a given type.  There is no constant
    3.39 +\isa{finite}.
    3.40  \end{warn}
    3.41  \index{sets|)}
    3.42  
    3.43 @@ -1077,4 +1076,4 @@
    3.44  two agents in a process algebra is an example of coinduction.
    3.45  The coinduction rule can be strengthened in various ways; see 
    3.46  theory \isa{Gfp} for details.  
    3.47 -\index{fixed points|)}
    3.48 \ No newline at end of file
    3.49 +\index{fixed points|)}
     4.1 --- a/doc-src/TutorialI/appendix.tex	Mon Mar 12 18:23:11 2001 +0100
     4.2 +++ b/doc-src/TutorialI/appendix.tex	Tue Mar 13 18:35:48 2001 +0100
     4.3 @@ -22,6 +22,15 @@
     4.4  \indexboldpos{\isasymequiv}{$IsaEq} &
     4.5  \ttindexboldpos{==}{$IsaEq} &
     4.6  \verb$\<equiv>$ \\
     4.7 +\indexboldpos{\isasymrightleftharpoons}{$IsaEqTrans} &
     4.8 +\ttindexboldpos{==}{$IsaEq} &
     4.9 +\verb$\<rightleftharpoons>$ \\
    4.10 +\indexboldpos{\isasymrightharpoonup}{$IsaEqTrans1} &
    4.11 +\ttindexboldpos{=>}{$IsaFun} &
    4.12 +\verb$\<rightharpoonup>$ \\
    4.13 +\indexboldpos{\isasymleftharpoondown}{$IsaEqTrans2} &
    4.14 +\ttindexboldpos{<=}{$IsaFun2} &
    4.15 +\verb$\<leftharpoondown>$ \\
    4.16  \indexboldpos{\isasymlambda}{$Isalam} &
    4.17  \texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
    4.18  \verb$\<lambda>$ \\
     5.1 --- a/doc-src/TutorialI/fp.tex	Mon Mar 12 18:23:11 2001 +0100
     5.2 +++ b/doc-src/TutorialI/fp.tex	Tue Mar 13 18:35:48 2001 +0100
     5.3 @@ -268,6 +268,8 @@
     5.4  
     5.5  \input{Misc/document/prime_def.tex}
     5.6  
     5.7 +\input{Misc/document/Translations.tex}
     5.8 +
     5.9  
    5.10  \section{The Definitional Approach}
    5.11  \label{sec:definitional}
    5.12 @@ -288,6 +290,8 @@
    5.13  as pure \isacommand{defs} are, but more convenient. And this is not just the
    5.14  case for \isacommand{primrec} but also for the other commands described
    5.15  later, like \isacommand{recdef} and \isacommand{inductive}.
    5.16 +This strict adherence to the definitional approach reduces the risk of 
    5.17 +soundness errors inside Isabelle/HOL.
    5.18  
    5.19  \chapter{More Functional Programming}
    5.20  
     6.1 --- a/doc-src/TutorialI/todo.tobias	Mon Mar 12 18:23:11 2001 +0100
     6.2 +++ b/doc-src/TutorialI/todo.tobias	Tue Mar 13 18:35:48 2001 +0100
     6.3 @@ -61,14 +61,13 @@
     6.4  differences between our HOL and the other one.
     6.5  
     6.6  Syntax translations! Harpoons already used!
     6.7 +say something about "abbreviations" when defs are introduced.
     6.8  
     6.9  warning: simp of asms from l to r; may require reordering (rotate_tac)
    6.10  
    6.11  Adjust FP textbook refs: new Bird, Hudak
    6.12  Discrete math textbook: Rosen?
    6.13  
    6.14 -say something about "abbreviations" when defs are introduced.
    6.15 -
    6.16  adjust type of ^ in tab:overloading
    6.17  
    6.18  an example of induction: !y. A --> B --> C ??