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/Ex/LetRec.thy
changeset 3197 25d11b449e92
parent 3192 14c7d7e29c44
child 3235 5ebd327ffb96 
--- a/Nominal/Ex/LetRec.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/LetRec.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -37,8 +37,8 @@
 | "height_trm (Lam v b) = 1 + (height_trm b)"
 | "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"
 | "height_bp (Bp v t) = height_trm t"
-  apply (simp only: eqvt_def height_trm_height_bp_graph_def)
-  apply (rule, perm_simp, rule, rule TrueI)
+  apply (simp add: eqvt_def height_trm_height_bp_graph_aux_def)
+  apply(rule TrueI)
   using [[simproc del: alpha_set]]
   apply auto
   apply (case_tac x)
nominal2