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/LocalWeakening.thy
changeset 35416 d8d7d1b785af
parent 29097 68245155eb58
child 41798 c3aa3c87ef21 
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -58,8 +58,7 @@
 by (induct t arbitrary: n rule: llam.induct)
    (simp_all add: perm_nat_def)
 
-constdefs
-  freshen :: "llam \<Rightarrow> name \<Rightarrow> llam"
+definition freshen :: "llam \<Rightarrow> name \<Rightarrow> llam" where
   "freshen t p \<equiv> vsub t 0 (lPar p)"
 
 lemma freshen_eqvt[eqvt]:
isabelle