# HG changeset patch
# User kleing
# Date 1117010595 -7200
# Node ID 9e569163ba8c2a16ef4f1465797905ac87073a1c
# Parent  794b37d08a2e70e1e927381f2d1dcf6640f9cda1
renamed search criterion 'rewrite' to 'simp'

diff -r 794b37d08a2e -r 9e569163ba8c doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed May 25 10:33:07 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed May 25 10:43:15 2005 +0200
@@ -1437,7 +1437,7 @@
   thmscontaining (('(' nat ')')?) (criterion *)
   ;
   criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
-    'rewrite' ':' term | term)
+    'simp' ':' term | term)
   ;
   thmdeps thmrefs
   ;
@@ -1471,13 +1471,13 @@
   packages, such as $\isarkeyword{datatype}$.
   
 \item [$\isarkeyword{thms_containing}~\vec c$] retrieves facts from the theory
-  or proof context matching all of the search criteria $\vec c$.  A criterion
+  or proof context matching all of the search criteria $\vec c$.  The criterion
   $name: s$ selects all theorems that contain $s$ in their fully qualified
   name.  The criteria $intro$, $elim$, and $dest$ select theorems that match
   the current goal as introduction, elimination or destruction rules,
-  respectively.  A criterion $rewrite: t$ selects all rewrite rules whose
-  left-hand side matches the given term.  A criterion term $t$ selects all
-  theorems that contain the pattern $t$ -- as usual patterns may contain
+  respectively.  The criterion $simp: t$ selects all rewrite rules whose
+  left-hand side matches the given term.  The criterion term $t$ selects all
+  theorems that contain the pattern $t$ -- as usual, patterns may contain
   occurrences of the dummy ``$\_$'', schematic variables, and type
   constraints.
   
diff -r 794b37d08a2e -r 9e569163ba8c src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Wed May 25 10:33:07 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Wed May 25 10:43:15 2005 +0200
@@ -11,7 +11,7 @@
 sig
   val find_thms: Proof.context -> FactIndex.spec -> (thmref * thm) list
   datatype 'term criterion =
-    Name of string | Intro | Elim | Dest | Rewrite of 'term | Pattern of 'term
+    Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term
   val print_theorems: Proof.context -> term option -> int option ->
     (bool * string criterion) list -> unit
 end;
@@ -83,13 +83,13 @@
 (** search criteria **)
 
 datatype 'term criterion =
-  Name of string | Intro | Elim | Dest | Rewrite of 'term | Pattern of 'term;
+  Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term;
 
 fun read_criterion _ (Name name) = Name name
   | read_criterion _ Intro = Intro
   | read_criterion _ Elim = Elim
   | read_criterion _ Dest = Dest
-  | read_criterion ctxt (Rewrite str) = Rewrite (ProofContext.read_term ctxt str)
+  | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term ctxt str)
   | read_criterion ctxt (Pattern str) =
       Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
 
@@ -102,7 +102,7 @@
     | Intro => Pretty.str (prfx "intro")
     | Elim => Pretty.str (prfx "elim")
     | Dest => Pretty.str (prfx "dest")
-    | Rewrite t => Pretty.block [Pretty.str (prfx "rewrite:"), Pretty.brk 1,
+    | Simp t => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
         Pretty.quote (ProofContext.pretty_term ctxt t)]
     | Pattern pat => Pretty.enclose (prfx " \"") "\""
         [ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat)])
@@ -172,14 +172,14 @@
 end;
 
 
-(* filter_rewrite *)
+(* filter_simp *)
 
-fun filter_rewrite ctxt t =
+fun filter_simp ctxt t =
   let
     val (_, {mk_rews = {mk, ...}, ...}) =
       MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt);
-    val extract_rewrite = (mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
-  in is_matching_thm extract_rewrite ctxt t end;
+    val extract_simp = (mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
+  in is_matching_thm extract_simp ctxt t end;
 
 
 (* filter_pattern *)
@@ -203,7 +203,7 @@
   | filter_crit ctxt (SOME goal) Intro = filter_intro ctxt goal
   | filter_crit ctxt (SOME goal) Elim = filter_elim ctxt goal
   | filter_crit ctxt (SOME goal) Dest = filter_dest ctxt goal
-  | filter_crit ctxt _ (Rewrite str) = filter_rewrite ctxt str
+  | filter_crit ctxt _ (Simp str) = filter_simp ctxt str
   | filter_crit ctxt _ (Pattern str) = filter_pattern ctxt str;
 
 in
diff -r 794b37d08a2e -r 9e569163ba8c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed May 25 10:33:07 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed May 25 10:43:15 2005 +0200
@@ -638,7 +638,7 @@
   P.reserved "intro" >> K FindTheorems.Intro ||
   P.reserved "elim" >> K FindTheorems.Elim ||
   P.reserved "dest" >> K FindTheorems.Dest ||
-  P.reserved "rewrite" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Rewrite ||
+  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
   P.term >> FindTheorems.Pattern;
 
 val find_theoremsP =