# HG changeset patch
# User kleing
# Date 1375368748 -7200
# Node ID 71fef62c4213132c420fa59645c0910a7ccd7547
# Parent  084ac81e987162023b10f07121eff5d8ce020496
removed duplicate lemma

diff -r 084ac81e9871 -r 71fef62c4213 src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Mon Jul 29 22:17:32 2013 +0200
+++ b/src/HOL/IMP/Fold.thy	Thu Aug 01 16:52:28 2013 +0200
@@ -7,7 +7,6 @@
 type_synonym
   tab = "vname \<Rightarrow> val option"
 
-(* maybe better as the composition of substitution and the existing simp_const(0) *)
 fun afold :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
 "afold (N n) _ = N n" |
 "afold (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
@@ -198,14 +197,11 @@
   "approx empty = (\<lambda>_. True)"
   by (auto simp: approx_def)
 
-lemma equiv_sym:
-  "c \<sim> c' \<longleftrightarrow> c' \<sim> c"
-  by (auto simp add: equiv_def)
 
 theorem constant_folding_equiv:
   "fold c empty \<sim> c"
   using approx_eq [of empty c]
-  by (simp add: equiv_up_to_True equiv_sym)
+  by (simp add: equiv_up_to_True sim_sym)
 
 
 
@@ -386,7 +382,7 @@
 theorem constant_folding_equiv':
   "fold' c empty \<sim> c"
   using fold'_equiv [of empty c]
-  by (simp add: equiv_up_to_True equiv_sym)
+  by (simp add: equiv_up_to_True sim_sym)
 
 
 end