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