Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simplified the proof.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 03 Feb 2010 14:39:19 +0100
changeset 1055 34220518cccf
parent 1054 68bdd5523608
child 1056 a9135d300fbf
Simplified the proof.
Quot/Nominal/Terms.thy file | annotate | diff | comparison | revisions 
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 14:36:48 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 14:39:19 2010 +0100
@@ -823,9 +823,8 @@
 sorry
 
 lemma bv_list_rsp:
-  shows "t \<approx>5 s \<Longrightarrow> True"
-  and "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
-apply(induct rule: alpha5_alphalts.inducts)
+  shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
+apply(induct rule: alpha5_alphalts.inducts(2))
 apply(simp_all)
 done
nominal2