--- 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
--- 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";
--- 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 *}
--- 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
--- 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}
--- 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}