1open HolKernel Parse boolLib bossLib; 2 3val _ = new_theory "caseEqAbbrev"; 4 5Type foo = ���:'a list��� 6 7Theorem bar: 8 (case x of [] => 0 | h::t => 3) = 4 ==> x <> [] 9Proof 10 simp[CaseEq"foo"] 11QED 12 13val _ = export_theory(); 14