From a94eac828280f06f6c34e9a62d88d41828e1db61 Mon Sep 17 00:00:00 2001 From: rsoeldner Date: Mon, 13 May 2024 19:36:01 +0200 Subject: [PATCH] add lowercase rewrite tactics --- src/1/Rewrite.sig | 4 ++++ src/1/Rewrite.sml | 5 +++++ 2 files changed, 9 insertions(+) diff --git a/src/1/Rewrite.sig b/src/1/Rewrite.sig index 889a46dd83..0f9023121f 100644 --- a/src/1/Rewrite.sig +++ b/src/1/Rewrite.sig @@ -37,15 +37,19 @@ sig val ONCE_ASM_REWRITE_RULE : thm list -> thm -> thm val PURE_REWRITE_TAC : thm list -> tactic + val pure_rewrite_tac : thm list -> tactic val REWRITE_TAC : thm list -> tactic val rewrite_tac : thm list -> tactic val PURE_ONCE_REWRITE_TAC : thm list -> tactic + val pure_once_rewrite_tac : thm list -> tactic val ONCE_REWRITE_TAC : thm list -> tactic val once_rewrite_tac : thm list -> tactic val PURE_ASM_REWRITE_TAC : thm list -> tactic + val pure_asm_rewrite_tac : thm list -> tactic val ASM_REWRITE_TAC : thm list -> tactic val asm_rewrite_tac : thm list -> tactic val PURE_ONCE_ASM_REWRITE_TAC : thm list -> tactic + val pure_once_asm_rewrite_tac : thm list -> tactic val ONCE_ASM_REWRITE_TAC : thm list -> tactic val once_asm_rewrite_tac : thm list -> tactic diff --git a/src/1/Rewrite.sml b/src/1/Rewrite.sml index 1e46ba8dd1..fa098e89a0 100644 --- a/src/1/Rewrite.sml +++ b/src/1/Rewrite.sml @@ -190,6 +190,7 @@ and ONCE_REWRITE_TAC thl = GEN_REWRITE_TAC Conv.ONCE_DEPTH_CONV (implicit_rewrites()) thl; val rewrite_tac = REWRITE_TAC and once_rewrite_tac = ONCE_REWRITE_TAC +val pure_rewrite_tac = PURE_REWRITE_TAC and pure_once_rewrite_tac = PURE_ONCE_REWRITE_TAC (* Rewrite a goal with the help of its assumptions *) @@ -203,6 +204,10 @@ and PURE_ONCE_ASM_REWRITE_TAC thl :tactic = and ONCE_ASM_REWRITE_TAC thl :tactic = Tactical.ASSUM_LIST (fn asl => ONCE_REWRITE_TAC (asl @ thl)); +val pure_asm_rewrite_tac = PURE_ASM_REWRITE_TAC +val pure_once_asm_rewrite_tac = PURE_ONCE_ASM_REWRITE_TAC + + val asm_rewrite_tac = ASM_REWRITE_TAC val once_asm_rewrite_tac = ONCE_ASM_REWRITE_TAC