--- 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.
--- 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
--- 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 =