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 syntax for "asm_lr" simplifier option.
authorberghofe
Mon, 30 Sep 2002 16:36:57 +0200
changeset 13605 528f7489a403
parent 13604 57bfacbbaeda
child 13606 2f121149acfe
Added syntax for "asm_lr" simplifier option.
src/Provers/simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/simplifier.ML	Mon Sep 30 16:34:56 2002 +0200
+++ b/src/Provers/simplifier.ML	Mon Sep 30 16:36:57 2002 +0200
@@ -475,6 +475,7 @@
 val no_asmN = "no_asm";
 val no_asm_useN = "no_asm_use";
 val no_asm_simpN = "no_asm_simp";
+val asm_lrN = "asm_lr";
 
 val simp_attr =
  (Attrib.add_del_args simp_add_global simp_del_global,
@@ -525,6 +526,7 @@
  (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
+  Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   Scan.succeed asm_full_simp_tac);
 
 val cong_modifiers =
isabelle