prefer xsymbol for book
authorkleing
Wed, 12 Jun 2013 20:52:09 -0700
changeset 52372 02dfb6bb487a
parent 52371 55908a74065f
child 52373 a231e6f89737
prefer xsymbol for book
src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Wed Jun 12 13:53:24 2013 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Wed Jun 12 20:52:09 2013 -0700
@@ -148,7 +148,7 @@
 text_raw{*\snip{BigStepEquiv}{0}{1}{% *}
 abbreviation
   equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
-  "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
+  "c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
 text_raw{*}%endsnip*}
 
 text {*