# HG changeset patch
# User berghofe
# Date 862584095 -7200
# Node ID a31170b673673b7851ec921da8288ac898d1af82
# Parent  ae362c99a635b0a1a10cf218f95d4ad6846dc147
Updated to LaTeX 2e

diff -r ae362c99a635 -r a31170b67367 doc-src/Ref/Makefile
--- a/doc-src/Ref/Makefile	Fri May 02 16:21:04 1997 +0200
+++ b/doc-src/Ref/Makefile	Fri May 02 16:41:35 1997 +0200
@@ -9,22 +9,22 @@
 FILES =  ref.tex introduction.tex goals.tex tactic.tex tctical.tex\
          thm.tex theories.tex defining.tex syntax.tex substitution.tex\
          simplifier.tex classical.tex theory-syntax.tex\
-	 ../rail.sty ../proof209.sty ../iman.sty ../extra.sty
+	 ../rail.sty ../proof.sty ../iman.sty ../extra.sty
 
 ref.dvi.gz:   $(FILES) 
 	-rm ref.dvi*
-	latex209 ref
+	latex ref
 	rail ref
 	bibtex ref
-	latex209 ref
-	latex209 ref
+	latex ref
+	latex ref
 	../sedindex ref
-	latex209 ref
+	latex ref
 	gzip -f ref.dvi
 
 dist:   $(FILES) 
 	-rm ref.dvi*
-	latex209 ref
-	latex209 ref
+	latex ref
+	latex ref
 	../sedindex ref
-	latex209 ref
+	latex ref
diff -r ae362c99a635 -r a31170b67367 doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Fri May 02 16:21:04 1997 +0200
+++ b/doc-src/Ref/defining.tex	Fri May 02 16:41:35 1997 +0200
@@ -469,8 +469,8 @@
 specifies no priorities.  The resulting production puts no priority
 constraints on any of its arguments and has maximal priority itself.
 Omitting priorities in this manner is prone to syntactic ambiguities unless
-the production's right-hand side is fully bracketed, as in \verb|"if _ then _
-else _ fi"|.
+the production's right-hand side is fully bracketed, as in
+\verb|"if _ then _ else _ fi"|.
 
 Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"},
 is sensible only if~$c$ is an identifier.  Otherwise you will be unable to
@@ -613,8 +613,8 @@
 
 The declaration is expanded internally to something like
 \begin{ttbox}
-\(c\)    :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
-"\(\Q\)"\hskip-3pt  :: [idts, \(\tau@2\)] => \(\tau@3\)   ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
+\(c\)\hskip3pt    :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
+"\(\Q\)"  :: [idts, \(\tau@2\)] => \(\tau@3\)   ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
 \end{ttbox}
 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
 \index{type constraints}
diff -r ae362c99a635 -r a31170b67367 doc-src/Ref/ref.rao
--- a/doc-src/Ref/ref.rao	Fri May 02 16:21:04 1997 +0200
+++ b/doc-src/Ref/ref.rao	Fri May 02 16:41:35 1997 +0200
@@ -1,329 +1,331 @@
-% This file was generated by 'rail' from 'ref.rai'
-\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()); \par name: id | string; \par extension : (section +) 'end' ( () | ml ); \par section : classes | default | types | arities | consts | constdefs | trans | defs | rules | oracle ; \par classes : 'classes' ( ( id ( () | '<' (id + ',') ) ) + ) ; \par default : 'default' sort ; \par sort : id | '\protect \relax $\mathsurround =\z@ \delimiter "4266308 $' (id * ',') '\protect \relax $\mathsurround =\z@ \delimiter "5267309 $' ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) nat; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id; \par \par arities : 'arities' ((( name + ',' ) '::' arity ) + ) ; \par arity : ( () | '(' (sort + ',') ')' ) id ; \par \par consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
+% This file was generated by '/usr/stud/berghofe/latex/rail/rail' from 'ref.rai'
+\rail@t {lbrace}
+\rail@t {rbrace}
+\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()); \par name: id | string; \par extension : (section +) 'end' ( () | ml ); \par section : classes | default | types | arities | consts | constdefs | trans | defs | rules | oracle ; \par classes : 'classes' ( ( id ( () | '<' (id + ',') ) ) + ) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) nat; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id; \par \par arities : 'arities' ((( name + ',' ) '::' arity ) + ) ; \par arity : ( () | '(' (sort + ',') ')' ) id ; \par \par consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
 \rail@o {1}{
 \rail@begin{2}{theoryDef}
-\rail@nont{id}
-\rail@term{=}
+\rail@nont{id}[]
+\rail@term{=}[]
 \rail@plus
-\rail@nont{name}
+\rail@nont{name}[]
 \rail@nextplus{1}
-\rail@cterm{+}
+\rail@cterm{+}[]
 \rail@endplus
 \rail@bar
-\rail@term{+}
-\rail@nont{extension}
+\rail@term{+}[]
+\rail@nont{extension}[]
 \rail@nextbar{1}
 \rail@endbar
 \rail@end
 \rail@begin{2}{name}
 \rail@bar
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextbar{1}
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@endbar
 \rail@end
 \rail@begin{2}{extension}
 \rail@plus
-\rail@nont{section}
+\rail@nont{section}[]
 \rail@nextplus{1}
 \rail@endplus
-\rail@term{end}
+\rail@term{end}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{ml}
+\rail@nont{ml}[]
 \rail@endbar
 \rail@end
 \rail@begin{10}{section}
 \rail@bar
-\rail@nont{classes}
+\rail@nont{classes}[]
 \rail@nextbar{1}
-\rail@nont{default}
+\rail@nont{default}[]
 \rail@nextbar{2}
-\rail@nont{types}
+\rail@nont{types}[]
 \rail@nextbar{3}
-\rail@nont{arities}
+\rail@nont{arities}[]
 \rail@nextbar{4}
-\rail@nont{consts}
+\rail@nont{consts}[]
 \rail@nextbar{5}
-\rail@nont{constdefs}
+\rail@nont{constdefs}[]
 \rail@nextbar{6}
-\rail@nont{trans}
+\rail@nont{trans}[]
 \rail@nextbar{7}
-\rail@nont{defs}
+\rail@nont{defs}[]
 \rail@nextbar{8}
-\rail@nont{rules}
+\rail@nont{rules}[]
 \rail@nextbar{9}
-\rail@nont{oracle}
+\rail@nont{oracle}[]
 \rail@endbar
 \rail@end
 \rail@begin{4}{classes}
-\rail@term{classes}
+\rail@term{classes}[]
 \rail@plus
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{<}
+\rail@term{<}[]
 \rail@plus
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextplus{2}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
 \rail@endbar
 \rail@nextplus{3}
 \rail@endplus
 \rail@end
 \rail@begin{1}{default}
-\rail@term{default}
-\rail@nont{sort}
+\rail@term{default}[]
+\rail@nont{sort}[]
 \rail@end
 \rail@begin{4}{sort}
 \rail@bar
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextbar{1}
-\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "4266308 $}
+\rail@token{lbrace}[]
 \rail@bar
 \rail@nextbar{2}
 \rail@plus
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextplus{3}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
 \rail@endbar
-\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "5267309 $}
+\rail@token{rbrace}[]
 \rail@endbar
 \rail@end
 \rail@begin{3}{types}
-\rail@term{types}
+\rail@term{types}[]
 \rail@plus
-\rail@nont{typeDecl}
+\rail@nont{typeDecl}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{(}
-\rail@nont{infix}
-\rail@term{)}
+\rail@term{(}[]
+\rail@nont{infix}[]
+\rail@term{)}[]
 \rail@endbar
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
 \rail@begin{2}{infix}
 \rail@bar
-\rail@term{infixr}
+\rail@term{infixr}[]
 \rail@nextbar{1}
-\rail@term{infixl}
+\rail@term{infixl}[]
 \rail@endbar
-\rail@nont{nat}
+\rail@nont{nat}[]
 \rail@end
 \rail@begin{3}{typeDecl}
-\rail@nont{typevarlist}
-\rail@nont{name}
+\rail@nont{typevarlist}[]
+\rail@nont{name}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{=}
+\rail@term{=}[]
 \rail@bar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@nextbar{2}
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@endbar
 \rail@endbar
 \rail@end
 \rail@begin{4}{typevarlist}
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{tid}
+\rail@nont{tid}[]
 \rail@nextbar{2}
-\rail@term{(}
+\rail@term{(}[]
 \rail@plus
-\rail@nont{tid}
+\rail@nont{tid}[]
 \rail@nextplus{3}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{)}
+\rail@term{)}[]
 \rail@endbar
 \rail@end
 \rail@begin{5}{type}
 \rail@bar
-\rail@nont{simpleType}
+\rail@nont{simpleType}[]
 \rail@nextbar{1}
-\rail@term{(}
-\rail@nont{type}
-\rail@term{)}
+\rail@term{(}[]
+\rail@nont{type}[]
+\rail@term{)}[]
 \rail@nextbar{2}
-\rail@nont{type}
-\rail@term{=>}
-\rail@nont{type}
+\rail@nont{type}[]
+\rail@term{=>}[]
+\rail@nont{type}[]
 \rail@nextbar{3}
-\rail@term{[}
+\rail@term{[}[]
 \rail@plus
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@nextplus{4}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{]}
-\rail@term{=>}
-\rail@nont{type}
+\rail@term{]}[]
+\rail@term{=>}[]
+\rail@nont{type}[]
 \rail@endbar
 \rail@end
 \rail@begin{6}{simpleType}
 \rail@bar
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextbar{1}
-\rail@nont{tid}
+\rail@nont{tid}[]
 \rail@bar
 \rail@nextbar{2}
-\rail@term{::}
-\rail@nont{id}
+\rail@term{::}[]
+\rail@nont{id}[]
 \rail@endbar
 \rail@nextbar{3}
-\rail@term{(}
+\rail@term{(}[]
 \rail@plus
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@nextplus{4}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{)}
-\rail@nont{id}
+\rail@term{)}[]
+\rail@nont{id}[]
 \rail@nextbar{5}
-\rail@nont{simpleType}
-\rail@nont{id}
+\rail@nont{simpleType}[]
+\rail@nont{id}[]
 \rail@endbar
 \rail@end
 \rail@begin{3}{arities}
-\rail@term{arities}
+\rail@term{arities}[]
 \rail@plus
 \rail@plus
-\rail@nont{name}
+\rail@nont{name}[]
 \rail@nextplus{1}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{::}
-\rail@nont{arity}
+\rail@term{::}[]
+\rail@nont{arity}[]
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
 \rail@begin{3}{arity}
 \rail@bar
 \rail@nextbar{1}
-\rail@term{(}
+\rail@term{(}[]
 \rail@plus
-\rail@nont{sort}
+\rail@nont{sort}[]
 \rail@nextplus{2}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{)}
+\rail@term{)}[]
 \rail@endbar
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@end
 \rail@begin{3}{consts}
-\rail@term{consts}
+\rail@term{consts}[]
 \rail@plus
-\rail@nont{constDecl}
+\rail@nont{constDecl}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{(}
-\rail@nont{mixfix}
-\rail@term{)}
+\rail@term{(}[]
+\rail@nont{mixfix}[]
+\rail@term{)}[]
 \rail@endbar
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
 \rail@begin{2}{constDecl}
 \rail@plus
-\rail@nont{name}
+\rail@nont{name}[]
 \rail@nextplus{1}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{::}
+\rail@term{::}[]
 \rail@bar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@nextbar{1}
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@endbar
 \rail@end
 \rail@begin{6}{mixfix}
 \rail@bar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@bar
 \rail@nextbar{2}
-\rail@term{[}
+\rail@term{[}[]
 \rail@plus
-\rail@nont{nat}
+\rail@nont{nat}[]
 \rail@nextplus{3}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{]}
+\rail@term{]}[]
 \rail@endbar
-\rail@nont{nat}
+\rail@nont{nat}[]
 \rail@endbar
 \rail@nextbar{4}
-\rail@nont{infix}
+\rail@nont{infix}[]
 \rail@nextbar{5}
-\rail@term{binder}
-\rail@nont{string}
-\rail@nont{nat}
+\rail@term{binder}[]
+\rail@nont{string}[]
+\rail@nont{nat}[]
 \rail@endbar
 \rail@end
 \rail@begin{3}{constdefs}
-\rail@term{constdefs}
+\rail@term{constdefs}[]
 \rail@plus
-\rail@nont{id}
-\rail@term{::}
+\rail@nont{id}[]
+\rail@term{::}[]
 \rail@bar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@nextbar{1}
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@endbar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
 \rail@begin{4}{trans}
-\rail@term{translations}
+\rail@term{translations}[]
 \rail@plus
-\rail@nont{pat}
+\rail@nont{pat}[]
 \rail@bar
-\rail@term{==}
+\rail@term{==}[]
 \rail@nextbar{1}
-\rail@term{=>}
+\rail@term{=>}[]
 \rail@nextbar{2}
-\rail@term{<=}
+\rail@term{<=}[]
 \rail@endbar
-\rail@nont{pat}
+\rail@nont{pat}[]
 \rail@nextplus{3}
 \rail@endplus
 \rail@end
 \rail@begin{2}{pat}
 \rail@bar
 \rail@nextbar{1}
-\rail@term{(}
-\rail@nont{id}
-\rail@term{)}
+\rail@term{(}[]
+\rail@nont{id}[]
+\rail@term{)}[]
 \rail@endbar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@end
 \rail@begin{2}{rules}
-\rail@term{rules}
+\rail@term{rules}[]
 \rail@plus
-\rail@nont{id}
-\rail@nont{string}
+\rail@nont{id}[]
+\rail@nont{string}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
 \rail@begin{2}{defs}
-\rail@term{defs}
+\rail@term{defs}[]
 \rail@plus
-\rail@nont{id}
-\rail@nont{string}
+\rail@nont{id}[]
+\rail@nont{string}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
 \rail@begin{1}{oracle}
-\rail@term{oracle}
-\rail@nont{name}
+\rail@term{oracle}[]
+\rail@nont{name}[]
 \rail@end
 \rail@begin{1}{ml}
-\rail@term{ML}
-\rail@nont{text}
+\rail@term{ML}[]
+\rail@nont{text}[]
 \rail@end
 }
diff -r ae362c99a635 -r a31170b67367 doc-src/Ref/ref.tex
--- a/doc-src/Ref/ref.tex	Fri May 02 16:21:04 1997 +0200
+++ b/doc-src/Ref/ref.tex	Fri May 02 16:41:35 1997 +0200
@@ -1,7 +1,9 @@
-\documentstyle[a4,12pt]{report}
+\documentclass[12pt]{report}
+\usepackage{a4}
+
 \makeatletter
 \input{../rail.sty}
-\input{../proof209.sty}
+\input{../proof.sty}
 \input{../iman.sty}
 \input{../extra.sty}
 \makeatother
@@ -38,6 +40,10 @@
 \sloppy
 \binperiod     %%%treat . like a binary operator
 
+\railalias{lbrace}{\{}
+\railalias{rbrace}{\}}
+\railterm{lbrace,rbrace}
+
 \begin{document}
 \index{definitions|see{rewriting, meta-level}}
 \index{rewriting!object-level|see{simplification}}
diff -r ae362c99a635 -r a31170b67367 doc-src/Ref/theory-syntax.tex
--- a/doc-src/Ref/theory-syntax.tex	Fri May 02 16:21:04 1997 +0200
+++ b/doc-src/Ref/theory-syntax.tex	Fri May 02 16:41:35 1997 +0200
@@ -49,7 +49,7 @@
         ;
 
 sort :  id
-     | '\{' (id * ',') '\}'
+     | lbrace (id * ',') rbrace
      ;
 
 types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )