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.
eliminated old-style inner comments;
authorwenzelm
Sun, 23 Sep 2018 19:17:57 +0200
changeset 69040 e0d14f648d46
parent 69039 51005671bee5
child 69041 d57c460ba112
eliminated old-style inner comments;
src/HOL/Data_Structures/Tree234_Map.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Data_Structures/Tree234_Map.thy	Sun Sep 23 17:14:06 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sun Sep 23 19:17:57 2018 +0200
@@ -66,7 +66,7 @@
    GT \<Rightarrow> (case cmp x (fst ab3) of
             LT \<Rightarrow> (case upd x y t3 of
                     T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
-                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
+                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2\<^cancel>\<open>q\<close> (Node3 t31 q t32 ab3 t4)) |
             EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
             GT \<Rightarrow> (case upd x y t4 of
                     T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
isabelle