Correctness via card, ugly proof from GCstep to step (up to renaming)
authorJoachim Breitner <mail@joachim-breitner.de>
Mon, 26 Jan 2015 09:39:21 +0000 (09:39 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Mon, 26 Jan 2015 09:39:21 +0000 (09:39 +0000)
commit0dd5c0def9617730d4cd60be06d7cd2f3908aa97
tree58d64338e6e89f0fb911d1b7b8218706ca7e3169
parenta93b726fa8c26496fcb18afda445fbad735c84fc
Correctness via card, ugly proof from GCstep to step (up to renaming)
Launchbury/ArityConsistent.thy
Launchbury/CallArityCorrectEnd2End.thy
Launchbury/CardinalityEtaExpandCorrect.thy
Launchbury/SestoftConf.thy
Launchbury/SestoftGC.thy