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/nominal_permeq.ML
changeset 55990 41c6b99c5fb7
parent 51717 9e7d1c139569
child 56230 3e449273942a 
--- a/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -241,7 +241,7 @@
 (* applies the ext-rule such that      *)
 (*                                     *)
 (*    f = g   goes to  /\x. f x = g x  *)
-fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
+fun ext_fun_tac i = ("extensionality expansion of functions", rtac @{thm ext} i);
 
 
 (* perm_extend_simp_tac_i is perm_simp plus additional tactics        *)
isabelle