Datatype.thy
author lcp
Thu, 18 Aug 1994 11:43:40 +0200
changeset 107 960e332d2e70
parent 53 5e0570ea8b70
permissions -rw-r--r--
HOL/Sum: rotated arguments of sum_case; added translation for case macro HOL/Sum: now has Part primitives, moved from ex/Simult, with extra laws from ZF/Sum

Datatype = Arith