# HG changeset patch
# User wenzelm
# Date 967487396 -7200
# Node ID bf65780eed024c4c710cbd65412c7a4e670f9b59
# Parent  f23bee3c068256a159fbae13997dfac79301cb15
added 'split' method;

diff -r f23bee3c0682 -r bf65780eed02 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Mon Aug 28 20:29:19 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Aug 28 20:29:56 2000 +0200
@@ -620,16 +620,19 @@
 
 \section{Basic equational reasoning}
 
-\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisaratt{symmetric}
+\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
 \begin{matharray}{rcl}
   subst & : & \isarmeth \\
   hypsubst^* & : & \isarmeth \\
+  split & : & \isarmeth \\
   symmetric & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
   'subst' thmref
   ;
+  'split' thmrefs
+  ;
 \end{rail}
 
 These methods and attributes provide basic facilities for equational reasoning
@@ -642,6 +645,9 @@
 \item [$subst~thm$] performs a single substitution step using rule $thm$,
   which may be either a meta or object equality.
 \item [$hypsubst$] performs substitution using some assumption.
+\item [$split~thms$] performs single-step case splitting using rules $thms$.
+  Note that the $simp$ method already involves repeated application of split
+  rules as declared in the current context (see \S\ref{sec:simp}).
 \item [$symmetric$] applies the symmetry rule of meta or object equality.
 \end{descr}
 
diff -r f23bee3c0682 -r bf65780eed02 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Mon Aug 28 20:29:19 2000 +0200
+++ b/src/Provers/splitter.ML	Mon Aug 28 20:29:56 2000 +0200
@@ -412,21 +412,22 @@
  (Attrib.add_del_args split_add_global split_del_global,
   Attrib.add_del_args split_add_local split_del_local);
 
-val setup_attrs =
-  Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")];
 
-
-(* method modifiers *)
+(* methods *)
 
 val split_modifiers =
  [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
   Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local),
   Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)];
 
+val split_meth = Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o split_tac);
+
 
 
 (** theory setup **)
 
-val setup = [setup_attrs];
+val setup =
+ [Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")],
+  Method.add_methods [(splitN, split_meth, "apply splitter rule")]];
 
 end;