Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Updated to LaTeX 2e
authorberghofe
Fri, 02 May 1997 16:41:35 +0200
changeset 3098 a31170b67367
parent 3097 ae362c99a635
child 3099 808681776bf7
Updated to LaTeX 2e
doc-src/Ref/Makefile file | annotate | diff | comparison | revisions
doc-src/Ref/defining.tex file | annotate | diff | comparison | revisions
doc-src/Ref/ref.rao file | annotate | diff | comparison | revisions
doc-src/Ref/ref.tex file | annotate | diff | comparison | revisions
doc-src/Ref/theory-syntax.tex file | annotate | diff | comparison | revisions 
--- 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
--- 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}
--- 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
 }
--- 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}}
--- 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 ')' ) ) + )
isabelle