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