doc-src/Contents
author berghofe
Fri, 21 Jul 2006 14:11:14 +0200
changeset 20173 c8f791af9a60
parent 18542 f42e544805f5
child 20950 981fa0ce23ed
permissions -rw-r--r--
Some cases in "case ... of ..." expressions may now be omitted (internally, these cases are assigned the "undefined" value).

Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar