Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/OptionalSugar.thy
changeset 63935 aa1fe1103ab8
parent 61955 e96292f32c3c 
--- a/src/HOL/Library/OptionalSugar.thy	Wed Sep 21 22:44:24 2016 +0200
+++ b/src/HOL/Library/OptionalSugar.thy	Thu Sep 22 00:12:17 2016 +0200
@@ -27,7 +27,7 @@
 
 (* append *)
 syntax (latex output)
-  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
+  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^latex>\<open>\\isacharat\<close>" 65)
 translations
   "_appendL xs ys" <= "xs @ ys" 
   "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
@@ -36,8 +36,8 @@
 (* deprecated, use thm with style instead, will be removed *)
 (* aligning equations *)
 notation (tab output)
-  "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
-  "Pure.eq"  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
+  "HOL.eq"  ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>=\<^latex>\<open>}\\putisatab\\isa{\<close> (_)" [50,49] 50) and
+  "Pure.eq"  ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>\<equiv>\<^latex>\<open>}\\putisatab\\isa{\<close> (_)")
 
 (* Let *)
 translations
isabelle