1open HolKernel Parse boolLib Datatype
2
3val _ = new_theory "foo"
4
5val _ = Hol_datatype`foo = Success | Failure`
6
7val _ = export_theory()
8