the records section
authorpaulson
Fri Jun 29 18:12:18 2001 +0200 (2001-06-29)
changeset 1138955e2aef8909b
parent 11388 5a32e6a78993
child 11390 735bf767833a
the records section
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Types/ROOT.ML
doc-src/TutorialI/Types/Records.thy
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/Types/types.tex
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Fri Jun 29 18:03:07 2001 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Fri Jun 29 18:12:18 2001 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4  HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz
     1.5  
     1.6  $(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
     1.7 -  Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \
     1.8 +  Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedef.thy \
     1.9    Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
    1.10    Types/Overloading.thy Types/Axioms.thy
    1.11  	$(REALUSEDIR) Types
     2.1 --- a/doc-src/TutorialI/Types/ROOT.ML	Fri Jun 29 18:03:07 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Types/ROOT.ML	Fri Jun 29 18:12:18 2001 +0200
     2.3 @@ -2,6 +2,7 @@
     2.4  use "../settings.ML";
     2.5  use_thy "Numbers";
     2.6  use_thy "Pairs";
     2.7 +use_thy "Records";
     2.8  use_thy "Typedef";
     2.9  use_thy "Overloading0";
    2.10  use_thy "Overloading2";
     3.1 --- a/doc-src/TutorialI/Types/Records.thy	Fri Jun 29 18:03:07 2001 +0200
     3.2 +++ b/doc-src/TutorialI/Types/Records.thy	Fri Jun 29 18:12:18 2001 +0200
     3.3 @@ -210,8 +210,7 @@
     3.4  text {* a polymorphic record equality (covers all possible extensions) *}
     3.5  lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Ycoord := b\<rparr> = r \<lparr>Ycoord := b\<rparr> \<lparr>Xcoord := a\<rparr>"
     3.6    -- "introduction of abstract record equality
     3.7 -         (order of updates doesn't affect the value, 
     3.8 -          though order of fields does the type)"
     3.9 +         (order of updates doesn't affect the value)"
    3.10  by simp
    3.11  
    3.12  lemma "r \<lparr>Xcoord := a, Ycoord := b\<rparr> = r \<lparr>Ycoord := b, Xcoord := a\<rparr>"
    3.13 @@ -220,7 +219,7 @@
    3.14  
    3.15  text {* Showing that repeated updates don't matter *}
    3.16  lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Xcoord := a'\<rparr> = r \<lparr>Xcoord := a'\<rparr>"
    3.17 -apply simp
    3.18 +by simp
    3.19  
    3.20  
    3.21  text {* surjective *}
     4.1 --- a/doc-src/TutorialI/Types/numerics.tex	Fri Jun 29 18:03:07 2001 +0200
     4.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jun 29 18:12:18 2001 +0200
     4.3 @@ -1,4 +1,8 @@
     4.4  % $Id$
     4.5 +
     4.6 +\section{Numbers}
     4.7 +\label{sec:numbers}
     4.8 +
     4.9  Until now, our numerical examples have used the type of \textbf{natural
    4.10  numbers},
    4.11  \isa{nat}.  This is a recursive datatype generated by the constructors
     5.1 --- a/doc-src/TutorialI/Types/types.tex	Fri Jun 29 18:03:07 2001 +0200
     5.2 +++ b/doc-src/TutorialI/Types/types.tex	Fri Jun 29 18:12:18 2001 +0200
     5.3 @@ -21,17 +21,14 @@
     5.4  The latter is fairly advanced: read the beginning to understand what it is
     5.5  about, but consult the rest only when necessary.
     5.6  
     5.7 -\section{Numbers}
     5.8 -\label{sec:numbers}
     5.9 -
    5.10  \input{Types/numerics}
    5.11  
    5.12  \index{pair|(}
    5.13  \input{Types/document/Pairs}
    5.14  \index{pair|)}
    5.15  
    5.16 -\section{Records}
    5.17 -\label{sec:records}
    5.18 +\input{Types/records}
    5.19 +
    5.20  
    5.21  \section{Axiomatic Type Classes}
    5.22  \label{sec:axclass}
     6.1 --- a/doc-src/TutorialI/tutorial.tex	Fri Jun 29 18:03:07 2001 +0200
     6.2 +++ b/doc-src/TutorialI/tutorial.tex	Fri Jun 29 18:12:18 2001 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  \documentclass{article}
     6.5  \newif\ifremarks
     6.6 -%\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
     6.7 -\remarksfalse
     6.8 +\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
     6.9 +%\remarksfalse
    6.10  \usepackage{cl2emono-modified,isabelle,isabellesym}
    6.11  \usepackage{../proof,amsmath,amsfonts}
    6.12  \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
    6.13 @@ -29,11 +29,6 @@
    6.14  %% lcp's macros
    6.15  \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
    6.16  \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
    6.17 -\let\bigisa=\isa
    6.18 -%% was previously
    6.19 -%% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}} 
    6.20 -%% because \isa is too small for variables, but does it really matter?
    6.21 -
    6.22  
    6.23  %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    6.24  %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}