Mercurial Mercurial > hg > nominal2 / 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.
Nominal/ExLet.thy
changeset 1658 aacab5f67333
parent 1653 a2142526bb01
child 1685 721d92623c9d 
--- a/Nominal/ExLet.thy	Fri Mar 26 16:46:40 2010 +0100
+++ b/Nominal/ExLet.thy	Fri Mar 26 17:01:22 2010 +0100
@@ -87,7 +87,7 @@
   apply (simp add: permute_bn_alpha_bn)
   apply (simp add: perm_bn[symmetric])
   apply (simp add: eqvts[symmetric])
-  apply (simp add: supp_Abs)
+  apply (simp add: supp_abs)
   apply (simp add: trm_lts.supp)
   apply (rule supp_perm_eq[symmetric])
   apply (subst supp_finite_atom_set)
@@ -157,10 +157,10 @@
     apply(rule at_set_avoiding2)
     apply(rule fin_bn)
     apply(simp add: finite_supp)
-    apply(simp add: supp_Abs)
+    apply(simp add: supp_abs)
     apply(rule finite_Diff)
     apply(simp add: finite_supp)
-    apply(simp add: fresh_star_def fresh_def supp_Abs)
+    apply(simp add: fresh_star_def fresh_def supp_abs)
     apply(simp add: eqvts permute_bn)
     apply(rule a5)
     apply(simp add: permute_bn)
nominal2