Theory Arch

(*  ID:         $Id: Arch.thy,v 1.2 2006/01/13 19:18:48 nipkow Exp $
    Author:     Tobias Nipkow
*)

header "Archive"

theory Arch
imports Main
uses ("arch.ML")
 ("Archives/Tri.ML")
 ("Archives/Quad.ML")
 ("Archives/Pent.ML")
 ("Archives/Hex.ML")
 ("Archives/Hept.ML")
 ("Archives/Oct.ML")
begin

text{* The Archive is contained in 6 ML files. *}

use "Archives/Tri.ML"
use "Archives/Quad.ML"
use "Archives/Pent.ML"
use "Archives/Hex.ML"
use "Archives/Hept.ML"
use "Archives/Oct.ML"

use "arch.ML"
setup {* add_archconstdefs *}

text{* First the ML values are loaded. Then they are turned into
Isabelle definitions of the constants @{const Tri}, @{const Quad},
@{const Pent}, @{const Hex}, @{const Hept}, @{const Oct}, all of type
@{typ"nat list list list"}. *}

end