src/HOL/Option.thy
author oheimb
Thu, 30 Oct 1997 14:18:14 +0100
changeset 4042 8abc33930ff0
parent 2019 b45d9f2042e0
child 4133 0a08c2b9b1ed
permissions -rw-r--r--
domain package: * minor changes to some names and values (for consistency), e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2019
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     1
(*  Title:      Option.thy
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     2
    ID:         $Id$
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     4
    Copyright   1994  TU Muenchen
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     5
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     6
Datatype 'a option
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     7
*)
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     8
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     9
Option = Arith +
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    10
datatype 'a option = None | Some 'a
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    11
end