doc-src/Tutorial/Datatype/lookupempty.ML
author paulson
Thu, 20 Feb 2003 11:09:48 +0100
changeset 13824 e4d8dea6dfc2
parent 9255 2ceb11a2e190
permissions -rw-r--r--
minor updates to pre-2002 release

Goal "lookup (Trie None []) as = None";
by(case_tac "as" 1);
by(Auto_tac);