From 2529f5a65d70dfffe40ead73ae49aaa4d78fefb4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 7 Jul 2018 22:47:28 +0100
Subject: Add some syntactic sugar for Isabelle

---
 src/state.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/state.ml b/src/state.ml
index e788ab6a..245d450c 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -367,15 +367,15 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) =
     let id' = remove_trailing_underscores id in
     separate_map hardline string [
       "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:";
-      "  \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\"";
+      "  \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = readS (" ^ id' ^ " \\<circ> regstate)\"";
       "  by (auto simp: liftState_read_reg_readS register_defs)";
       "";
       "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:";
-      "  \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
+      "  \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
       "  by (auto simp: liftState_write_reg_updateS register_defs)"
     ]
   in
-  string "abbreviation \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^
+  string "abbreviation liftS (\"\\<lbrakk>_\\<rbrakk>\\<^sub>S\") where \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^
   hardline ^^ hardline ^^
   register_defs ^^
   hardline ^^ hardline ^^
-- 
cgit v1.2.3