Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added elim_vars to preprocessor.
authorberghofe
Mon, 30 Sep 2002 16:10:32 +0200
changeset 13599 cfdf7e4cd0d2
parent 13598 8bc77b17f59f
child 13600 9702c8636a7b
Added elim_vars to preprocessor.
src/HOL/Extraction.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction.thy	Mon Sep 30 16:09:05 2002 +0200
+++ b/src/HOL/Extraction.thy	Mon Sep 30 16:10:32 2002 +0200
@@ -19,7 +19,8 @@
         ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
           ProofRewriteRules.rprocs true) o
       Proofterm.rewrite_proof (Sign.tsig_of sg)
-        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true)))
+        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
+      ProofRewriteRules.elim_vars (curry Const "arbitrary")))
 *}
 
 lemmas [extraction_expand] =
isabelle