src/HOLCF/Ssum.thy
changeset 15600 a59f07556a8d
parent 15593 24d770bbc44a
child 15606 95617b30514b
equal deleted inserted replaced
15599:10cedbd5289e 15600:a59f07556a8d
     1 (*  Title:      HOLCF/Ssum0.thy
     1 (*  Title:      HOLCF/Ssum.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     5 
     6 Strict sum with typedef
     6 Strict sum with typedef