# HG changeset patch
# User wenzelm
# Date 863015913 -7200
# Node ID dd3666cbc76483a77b45230d0ea24ad382af6b38
# Parent  d01d4c0c4b4400190ad21a93fee4795c4f358436
SYNC;

diff -r d01d4c0c4b44 -r dd3666cbc764 doc-src/Intro/intro.ind
--- a/doc-src/Intro/intro.ind	Wed May 07 16:29:06 1997 +0200
+++ b/doc-src/Intro/intro.ind	Wed May 07 16:38:33 1997 +0200
@@ -39,6 +39,7 @@
     \subitem Prolog style, 62
   \item {\tt bd}, 31
   \item {\tt be}, 31
+  \item {\tt Blast_tac}, 39
   \item {\tt br}, 31
   \item {\tt by}, 30
 
@@ -87,7 +88,6 @@
   \indexspace
 
   \item {\tt FalseE} theorem, 45
-  \item {\tt fast_tac}, 39
   \item first-order logic, 1
   \item flex-flex constraints, 6, 25, \bold{28}
   \item {\tt flexflex_rule}, 29
diff -r d01d4c0c4b44 -r dd3666cbc764 doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Wed May 07 16:29:06 1997 +0200
+++ b/doc-src/Ref/ref.ind	Wed May 07 16:38:33 1997 +0200
@@ -470,7 +470,7 @@
   \item {\tt PROP} symbol, 65
   \item {\tt prop} nonterminal, \bold{64}, 76
   \item {\tt prop} type, 60, 66
-  \item {\tt prove_goal}, 10, \bold{12}
+  \item {\tt prove_goal}, 10, \bold{13}
   \item {\tt prove_goalw}, \bold{13}
   \item {\tt prove_goalw_cterm}, \bold{13}
   \item {\tt prth}, \bold{36}
diff -r d01d4c0c4b44 -r dd3666cbc764 doc-src/Ref/ref.rao
--- a/doc-src/Ref/ref.rao	Wed May 07 16:29:06 1997 +0200
+++ b/doc-src/Ref/ref.rao	Wed May 07 16:38:33 1997 +0200
@@ -1,7 +1,7 @@
 % This file was generated by '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 | syntax | trans | defs | constdefs | rules | axclass | instance | oracle ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (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 arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | ( 'infixr' | 'infixl' ) (() | string) nat | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | ((string | longident) + ',')) (() | verbatim) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
+\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (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 arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | ( 'infixr' | 'infixl' ) (() | string) nat | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
 \rail@o {1}{
 \rail@begin{2}{theoryDef}
 \rail@nont{id}[]
@@ -389,6 +389,7 @@
 \rail@begin{4}{witness}
 \rail@bar
 \rail@nextbar{1}
+\rail@term{(}[]
 \rail@plus
 \rail@bar
 \rail@nont{string}[]
@@ -398,6 +399,7 @@
 \rail@nextplus{3}
 \rail@cterm{,}[]
 \rail@endplus
+\rail@term{)}[]
 \rail@endbar
 \rail@bar
 \rail@nextbar{1}