1open HolKernel Parse boolLib 2 3open inheritCase1Theory 4val _ = new_theory "inheritCase2"; 5val _ = set_grammar_ancestry ["inheritCase1"] 6 7val _ = current_backend := PPBackEnd.raw_terminal 8val _ = new_constant("len", ``:'a list -> num``) 9val s = PP.pp_to_string 70 pp_term 10 ``case x of Nil => 0 | Cons h t => h + len t`` 11 12val _ = assert (equal "case x of Nil => 0 | Cons h t => h + len t") s 13 14val _ = export_theory(); 15