src/HOL/Plain.thy
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 27368 9f90ac19e32b
child 29304 5c71a6da989d
permissions -rw-r--r--
named code theorem for Fract_norm
     1 (*  Title:      HOL/Plain.thy
     2     ID:         $Id$
     3 
     4 Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
     5 *)
     6 
     7 header {* Plain HOL *}
     8 
     9 theory Plain
    10 imports Datatype FunDef Record SAT Extraction
    11 begin
    12 
    13 ML {* path_add "~~/src/HOL/Library" *}
    14 
    15 end