# HG changeset patch
# User paulson
# Date 993831138 -7200
# Node ID 55e2aef8909b4b67e28ed75c5c930db684f738ff
# Parent  5a32e6a789931dec7df45cd3ea3ad8a65cbcd925
the records section

diff -r 5a32e6a78993 -r 55e2aef8909b doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Fri Jun 29 18:03:07 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Fri Jun 29 18:12:18 2001 +0200
@@ -154,7 +154,7 @@
 HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz
 
 $(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
-  Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \
+  Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedef.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
 	$(REALUSEDIR) Types
diff -r 5a32e6a78993 -r 55e2aef8909b doc-src/TutorialI/Types/ROOT.ML
--- a/doc-src/TutorialI/Types/ROOT.ML	Fri Jun 29 18:03:07 2001 +0200
+++ b/doc-src/TutorialI/Types/ROOT.ML	Fri Jun 29 18:12:18 2001 +0200
@@ -2,6 +2,7 @@
 use "../settings.ML";
 use_thy "Numbers";
 use_thy "Pairs";
+use_thy "Records";
 use_thy "Typedef";
 use_thy "Overloading0";
 use_thy "Overloading2";
diff -r 5a32e6a78993 -r 55e2aef8909b doc-src/TutorialI/Types/Records.thy
--- a/doc-src/TutorialI/Types/Records.thy	Fri Jun 29 18:03:07 2001 +0200
+++ b/doc-src/TutorialI/Types/Records.thy	Fri Jun 29 18:12:18 2001 +0200
@@ -210,8 +210,7 @@
 text {* a polymorphic record equality (covers all possible extensions) *}
 lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Ycoord := b\<rparr> = r \<lparr>Ycoord := b\<rparr> \<lparr>Xcoord := a\<rparr>"
   -- "introduction of abstract record equality
-         (order of updates doesn't affect the value, 
-          though order of fields does the type)"
+         (order of updates doesn't affect the value)"
 by simp
 
 lemma "r \<lparr>Xcoord := a, Ycoord := b\<rparr> = r \<lparr>Ycoord := b, Xcoord := a\<rparr>"
@@ -220,7 +219,7 @@
 
 text {* Showing that repeated updates don't matter *}
 lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Xcoord := a'\<rparr> = r \<lparr>Xcoord := a'\<rparr>"
-apply simp
+by simp
 
 
 text {* surjective *}
diff -r 5a32e6a78993 -r 55e2aef8909b doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Fri Jun 29 18:03:07 2001 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jun 29 18:12:18 2001 +0200
@@ -1,4 +1,8 @@
 % $Id$
+
+\section{Numbers}
+\label{sec:numbers}
+
 Until now, our numerical examples have used the type of \textbf{natural
 numbers},
 \isa{nat}.  This is a recursive datatype generated by the constructors
diff -r 5a32e6a78993 -r 55e2aef8909b doc-src/TutorialI/Types/types.tex
--- a/doc-src/TutorialI/Types/types.tex	Fri Jun 29 18:03:07 2001 +0200
+++ b/doc-src/TutorialI/Types/types.tex	Fri Jun 29 18:12:18 2001 +0200
@@ -21,17 +21,14 @@
 The latter is fairly advanced: read the beginning to understand what it is
 about, but consult the rest only when necessary.
 
-\section{Numbers}
-\label{sec:numbers}
-
 \input{Types/numerics}
 
 \index{pair|(}
 \input{Types/document/Pairs}
 \index{pair|)}
 
-\section{Records}
-\label{sec:records}
+\input{Types/records}
+
 
 \section{Axiomatic Type Classes}
 \label{sec:axclass}
diff -r 5a32e6a78993 -r 55e2aef8909b doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Fri Jun 29 18:03:07 2001 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Fri Jun 29 18:12:18 2001 +0200
@@ -1,7 +1,7 @@
 \documentclass{article}
 \newif\ifremarks
-%\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
-\remarksfalse
+\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
+%\remarksfalse
 \usepackage{cl2emono-modified,isabelle,isabellesym}
 \usepackage{../proof,amsmath,amsfonts}
 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
@@ -29,11 +29,6 @@
 %% lcp's macros
 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
-\let\bigisa=\isa
-%% was previously
-%% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}} 
-%% because \isa is too small for variables, but does it really matter?
-
 
 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
 %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}