--- a/doc-src/Ref/Makefile Thu Feb 20 14:59:02 1997 +0100
+++ b/doc-src/Ref/Makefile Thu Feb 20 15:13:52 1997 +0100
@@ -9,10 +9,10 @@
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\
- ../iman.sty ../extra.sty
+ ../proof209.sty ../iman.sty ../extra.sty
ref.dvi.gz: $(FILES)
- -rm ref.dvi.gz
+ -rm ref.dvi*
latex209 ref
rail ref
bibtex ref
@@ -21,3 +21,10 @@
../sedindex ref
latex209 ref
gzip -f ref.dvi
+
+dist: $(FILES)
+ -rm ref.dvi*
+ latex209 ref
+ latex209 ref
+ ../sedindex ref
+ latex209 ref
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/ref.rao Thu Feb 20 15:13:52 1997 +0100
@@ -0,0 +1,329 @@
+% 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 }
+\rail@o {1}{
+\rail@begin{2}{theoryDef}
+\rail@nont{id}
+\rail@term{=}
+\rail@plus
+\rail@nont{name}
+\rail@nextplus{1}
+\rail@cterm{+}
+\rail@endplus
+\rail@bar
+\rail@term{+}
+\rail@nont{extension}
+\rail@nextbar{1}
+\rail@endbar
+\rail@end
+\rail@begin{2}{name}
+\rail@bar
+\rail@nont{id}
+\rail@nextbar{1}
+\rail@nont{string}
+\rail@endbar
+\rail@end
+\rail@begin{2}{extension}
+\rail@plus
+\rail@nont{section}
+\rail@nextplus{1}
+\rail@endplus
+\rail@term{end}
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{ml}
+\rail@endbar
+\rail@end
+\rail@begin{10}{section}
+\rail@bar
+\rail@nont{classes}
+\rail@nextbar{1}
+\rail@nont{default}
+\rail@nextbar{2}
+\rail@nont{types}
+\rail@nextbar{3}
+\rail@nont{arities}
+\rail@nextbar{4}
+\rail@nont{consts}
+\rail@nextbar{5}
+\rail@nont{constdefs}
+\rail@nextbar{6}
+\rail@nont{trans}
+\rail@nextbar{7}
+\rail@nont{defs}
+\rail@nextbar{8}
+\rail@nont{rules}
+\rail@nextbar{9}
+\rail@nont{oracle}
+\rail@endbar
+\rail@end
+\rail@begin{4}{classes}
+\rail@term{classes}
+\rail@plus
+\rail@nont{id}
+\rail@bar
+\rail@nextbar{1}
+\rail@term{<}
+\rail@plus
+\rail@nont{id}
+\rail@nextplus{2}
+\rail@cterm{,}
+\rail@endplus
+\rail@endbar
+\rail@nextplus{3}
+\rail@endplus
+\rail@end
+\rail@begin{1}{default}
+\rail@term{default}
+\rail@nont{sort}
+\rail@end
+\rail@begin{4}{sort}
+\rail@bar
+\rail@nont{id}
+\rail@nextbar{1}
+\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "4266308 $}
+\rail@bar
+\rail@nextbar{2}
+\rail@plus
+\rail@nont{id}
+\rail@nextplus{3}
+\rail@cterm{,}
+\rail@endplus
+\rail@endbar
+\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "5267309 $}
+\rail@endbar
+\rail@end
+\rail@begin{3}{types}
+\rail@term{types}
+\rail@plus
+\rail@nont{typeDecl}
+\rail@bar
+\rail@nextbar{1}
+\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@nextbar{1}
+\rail@term{infixl}
+\rail@endbar
+\rail@nont{nat}
+\rail@end
+\rail@begin{3}{typeDecl}
+\rail@nont{typevarlist}
+\rail@nont{name}
+\rail@bar
+\rail@nextbar{1}
+\rail@term{=}
+\rail@bar
+\rail@nont{string}
+\rail@nextbar{2}
+\rail@nont{type}
+\rail@endbar
+\rail@endbar
+\rail@end
+\rail@begin{4}{typevarlist}
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{tid}
+\rail@nextbar{2}
+\rail@term{(}
+\rail@plus
+\rail@nont{tid}
+\rail@nextplus{3}
+\rail@cterm{,}
+\rail@endplus
+\rail@term{)}
+\rail@endbar
+\rail@end
+\rail@begin{5}{type}
+\rail@bar
+\rail@nont{simpleType}
+\rail@nextbar{1}
+\rail@term{(}
+\rail@nont{type}
+\rail@term{)}
+\rail@nextbar{2}
+\rail@nont{type}
+\rail@term{=>}
+\rail@nont{type}
+\rail@nextbar{3}
+\rail@term{[}
+\rail@plus
+\rail@nont{type}
+\rail@nextplus{4}
+\rail@cterm{,}
+\rail@endplus
+\rail@term{]}
+\rail@term{=>}
+\rail@nont{type}
+\rail@endbar
+\rail@end
+\rail@begin{6}{simpleType}
+\rail@bar
+\rail@nont{id}
+\rail@nextbar{1}
+\rail@nont{tid}
+\rail@bar
+\rail@nextbar{2}
+\rail@term{::}
+\rail@nont{id}
+\rail@endbar
+\rail@nextbar{3}
+\rail@term{(}
+\rail@plus
+\rail@nont{type}
+\rail@nextplus{4}
+\rail@cterm{,}
+\rail@endplus
+\rail@term{)}
+\rail@nont{id}
+\rail@nextbar{5}
+\rail@nont{simpleType}
+\rail@nont{id}
+\rail@endbar
+\rail@end
+\rail@begin{3}{arities}
+\rail@term{arities}
+\rail@plus
+\rail@plus
+\rail@nont{name}
+\rail@nextplus{1}
+\rail@cterm{,}
+\rail@endplus
+\rail@term{::}
+\rail@nont{arity}
+\rail@nextplus{2}
+\rail@endplus
+\rail@end
+\rail@begin{3}{arity}
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}
+\rail@plus
+\rail@nont{sort}
+\rail@nextplus{2}
+\rail@cterm{,}
+\rail@endplus
+\rail@term{)}
+\rail@endbar
+\rail@nont{id}
+\rail@end
+\rail@begin{3}{consts}
+\rail@term{consts}
+\rail@plus
+\rail@nont{constDecl}
+\rail@bar
+\rail@nextbar{1}
+\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@nextplus{1}
+\rail@cterm{,}
+\rail@endplus
+\rail@term{::}
+\rail@bar
+\rail@nont{string}
+\rail@nextbar{1}
+\rail@nont{type}
+\rail@endbar
+\rail@end
+\rail@begin{6}{mixfix}
+\rail@bar
+\rail@nont{string}
+\rail@bar
+\rail@nextbar{1}
+\rail@bar
+\rail@nextbar{2}
+\rail@term{[}
+\rail@plus
+\rail@nont{nat}
+\rail@nextplus{3}
+\rail@cterm{,}
+\rail@endplus
+\rail@term{]}
+\rail@endbar
+\rail@nont{nat}
+\rail@endbar
+\rail@nextbar{4}
+\rail@nont{infix}
+\rail@nextbar{5}
+\rail@term{binder}
+\rail@nont{string}
+\rail@nont{nat}
+\rail@endbar
+\rail@end
+\rail@begin{3}{constdefs}
+\rail@term{constdefs}
+\rail@plus
+\rail@nont{id}
+\rail@term{::}
+\rail@bar
+\rail@nont{string}
+\rail@nextbar{1}
+\rail@nont{type}
+\rail@endbar
+\rail@nont{string}
+\rail@nextplus{2}
+\rail@endplus
+\rail@end
+\rail@begin{4}{trans}
+\rail@term{translations}
+\rail@plus
+\rail@nont{pat}
+\rail@bar
+\rail@term{==}
+\rail@nextbar{1}
+\rail@term{=>}
+\rail@nextbar{2}
+\rail@term{<=}
+\rail@endbar
+\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@endbar
+\rail@nont{string}
+\rail@end
+\rail@begin{2}{rules}
+\rail@term{rules}
+\rail@plus
+\rail@nont{id}
+\rail@nont{string}
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{defs}
+\rail@term{defs}
+\rail@plus
+\rail@nont{id}
+\rail@nont{string}
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{1}{oracle}
+\rail@term{oracle}
+\rail@nont{name}
+\rail@end
+\rail@begin{1}{ml}
+\rail@term{ML}
+\rail@nont{text}
+\rail@end
+}
--- a/doc-src/Ref/ref.tex Thu Feb 20 14:59:02 1997 +0100
+++ b/doc-src/Ref/ref.tex Thu Feb 20 15:13:52 1997 +0100
@@ -1,4 +1,10 @@
-\documentstyle[a4,12pt,rail,proof209,iman,extra]{report}
+\documentstyle[a4,12pt,rail]{report}
+\makeatletter
+\input{../proof209.sty}
+\input{../iman.sty}
+\input{../extra.sty}
+\makeatother
+
%% $Id$
%%\includeonly{}
%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1}