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/Nominal/Examples/SOS.thy
changeset 26806 40b411ec05aa
parent 25867 c24395ea4e71
child 26966 071f40487734 
--- a/src/HOL/Nominal/Examples/SOS.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Wed May 07 10:57:19 2008 +0200
@@ -422,7 +422,7 @@
   shows "(pi\<bullet>x)\<in>V T"
 using a
 apply(nominal_induct T arbitrary: pi x rule: ty.induct)
-apply(auto simp add: trm.inject perm_set_def)
+apply(auto simp add: trm.inject)
 apply(simp add: eqvts)
 apply(rule_tac x="pi\<bullet>xa" in exI)
 apply(rule_tac x="pi\<bullet>e" in exI)
isabelle