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