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/ExCoreHaskell.thy
changeset 1667 2922b04d9545
parent 1658 aacab5f67333
child 1684 b9e4c812d2c6
child 1687 51bc795b81fd 
--- a/Nominal/ExCoreHaskell.thy	Fri Mar 26 22:23:22 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Sat Mar 27 06:44:14 2010 +0100
@@ -312,7 +312,7 @@
 apply (simp)
 oops
 
-lemma 
+lemma strong_inudction_principle:
   assumes a01: "\<And>b. P1 b KStar"
   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
nominal2