src/HOL/Main.thy
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 28263 69eaa97e7e96
child 29304 5c71a6da989d
permissions -rw-r--r--
named code theorem for Fract_norm
webertj@17602
     1
(*  Title:      HOL/Main.thy
webertj@17602
     2
    ID:         $Id$
webertj@17602
     3
*)
wenzelm@9619
     4
wenzelm@12024
     5
header {* Main HOL *}
wenzelm@12024
     6
nipkow@15131
     7
theory Main
haftmann@28228
     8
imports Plain Code_Eval Map Nat_Int_Bij Recdef
nipkow@15131
     9
begin
wenzelm@9650
    10
haftmann@27367
    11
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
haftmann@25964
    12
wenzelm@9650
    13
end