src/HOL/Word/ROOT.ML
author huffman
Mon, 20 Aug 2007 17:31:01 +0200
changeset 24337 b31565d12ec8
parent 24333 e77ea0ea7f2c
child 24443 ab6206ccb570
permissions -rw-r--r--
no_document for Infinite_Set, Parity

no_document use_thys ["Infinite_Set", "Parity"];
use_thy "WordExamples";