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
haftmann@27368
     1
(*  Title:      HOL/Plain.thy
haftmann@27368
     2
    ID:         $Id$
haftmann@27368
     3
haftmann@27368
     4
Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
haftmann@27368
     5
*)
haftmann@27368
     6
haftmann@27368
     7
header {* Plain HOL *}
haftmann@27368
     8
haftmann@27368
     9
theory Plain
haftmann@27368
    10
imports Datatype FunDef Record SAT Extraction
haftmann@27368
    11
begin
haftmann@27368
    12
haftmann@27368
    13
ML {* path_add "~~/src/HOL/Library" *}
haftmann@27368
    14
haftmann@27368
    15
end