# HG changeset patch
# User wenzelm
# Date 966501140 -7200
# Node ID b80ea2b32f8ee4b83e0bf487a505cbd02d43c4db
# Parent  6eafc4d2ed851304b1a24ec1481b0de53bc4e6bc
cases/induct method: 'opaque' by default; added 'open' option;

diff -r 6eafc4d2ed85 -r b80ea2b32f8e doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Thu Aug 17 10:31:43 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Thu Aug 17 10:32:20 2000 +0200
@@ -214,9 +214,9 @@
 about large specifications.
 
 \begin{rail}
-  'cases' ('(simplified)')? ('(opaque)')? \\ (insts * 'and') rule?  ;
+  'cases' ('(simplified)')? ('(open)')? \\ (insts * 'and') rule?  ;
 
-  'induct' ('(stripped)')? ('(opaque)')? \\ (insts * 'and') rule?
+  'induct' ('(stripped)')? ('(open)')? \\ (insts * 'and') rule?
   ;
 
   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
@@ -247,14 +247,13 @@
   The $simplified$ option causes ``obvious cases'' of the rule to be solved
   beforehand, while the others are left unscathed.
   
-  The $opaque$ option causes the parameters of the new local contexts to be
-  turned into ``internal'' names.  This results in quasi-existentially bound
-  elements to be introduced when individual cases are invoked later.  Thus
-  both unwanted hiding of existing local variables and references to
-  implicitly bound variables (stemming from cases) are avoided.  So by using
-  the $opaque$ option, a proof text may become slightly more readable and
-  robust.
-  
+  The $open$ option causes the parameters of the new local contexts to be
+  exposed to the current proof context.  Thus local variables stemming from
+  distant parts of the theory development may be introduced in an implicit
+  manner, which can be quite confusing to the reader.  Furthermore, this
+  option may cause unwanted hiding of existing local variables, resulting in
+  less robust proof texts.
+
 \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
   induction rules, which are determined as follows:
   \begin{matharray}{llll}
@@ -276,8 +275,7 @@
   application of the induction rule.  This accommodates typical
   ``strengthening of induction'' predicates.
   
-  The $opaque$ option has the same effect as for the $cases$ method, see
-  above.
+  The $open$ option has the same effect as for the $cases$ method, see above.
 \end{descr}
 
 Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
@@ -324,11 +322,11 @@
 \subsection{Emulating tactic scripts}\label{sec:induct_tac}
 
 \indexisarmeth{case-tac}\indexisarmeth{induct-tac}
-\indexisarmeth{mk-cases-tac}\indexisarcmd{inductive-cases}
+\indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
 \begin{matharray}{rcl}
-  case_tac & : & \isarmeth \\
-  induct_tac & : & \isarmeth \\
-  mk_cases_tac & : & \isarmeth \\
+  case_tac^* & : & \isarmeth \\
+  induct_tac^* & : & \isarmeth \\
+  ind_cases^* & : & \isarmeth \\
   \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
@@ -338,20 +336,20 @@
 \railalias{inducttac}{induct\_tac}
 \railterm{inducttac}
 
-\railalias{mkcasestac}{mk\_cases\_tac}
-\railterm{mkcasestac}
+\railalias{indcases}{ind\_cases}
+\railterm{indcases}
 
-\railalias{indcases}{inductive\_cases}
-\railterm{indcases}
+\railalias{inductivecases}{inductive\_cases}
+\railterm{inductivecases}
 
 \begin{rail}
   casetac goalspec? term rule?
   ;
   inducttac goalspec? (insts * 'and') rule?
   ;
-  mkcasestac (prop +)
+  indcases (prop +)
   ;
-  indcases thmdef? (prop +) comment?
+  inductivecases thmdecl? (prop +) comment?
   ;
 
   rule: ('rule' ':' thmref)
@@ -368,13 +366,13 @@
   proper $induct$ and $cases$ proof methods (see
   \S\ref{sec:induct-method-proper}).
   
-\item [$mk_cases_tac$ and $\isarkeyword{inductive_cases}$] provide an
-  interface to the \texttt{mk_cases} operation.  Rules are simplified in an
-  unrestricted forward manner, unlike the proper $cases$ method (see
+\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
+  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
+  forward manner, unlike the proper $cases$ method (see
   \S\ref{sec:induct-method-proper}) which requires simplified cases to be
   solved completely.
   
-  While $mk_cases_tac$ is a proof method to apply the result immediately as
+  While $ind_cases$ is a proof method to apply the result immediately as
   elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   theorems at the theory level for later use,
 \end{descr}