author paulson
Fri, 01 Apr 2005 11:12:39 +0200
changeset 15645 5e20c54683d3
parent 15382 e56ce5cefe9c
child 15653 3549ff7158f3
permissions -rw-r--r--
patch to get it working again

(*  Title:      HOL/Reconstruction.thy
    ID: $Id$
    Author:     Lawrence C Paulson
    Copyright   2004  University of Cambridge

header{*Attributes for Reconstructing External Resolution Proofs*}

theory Reconstruction
    imports Hilbert_Choice Map Infinite_Set
    files "Tools/res_lib.ML"


text{*Every theory of HOL must be a descendant or ancestor of this one!*}

setup Reconstruction.setup