Up to index of Isabelle/HOL/Tame
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