Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_syn.ML
changeset 16074 9e569163ba8c
parent 16038 b645ff0c697c
child 16102 c5f6726d9bb1 
--- 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 =
isabelle