1open HolKernel Parse boolLib
2
3open Datatype
4
5val _ = new_theory "inheritCase1";
6
7val _ = Datatype`list = Nil | Cons 'a list`;
8
9val _ = export_theory();
10