src/HOL/Reconstruction.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15382 e56ce5cefe9c
child 15645 5e20c54683d3
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/Reconstruction.thy
     2     ID: $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   2004  University of Cambridge
     5 *)
     6 
     7 header{*Attributes for Reconstructing External Resolution Proofs*}
     8 
     9 theory Reconstruction
    10     imports Hilbert_Choice Map Infinite_Set
    11     files "Tools/res_lib.ML"
    12 	  "Tools/res_clause.ML"
    13 	  "Tools/res_skolem_function.ML"
    14 	  "Tools/res_axioms.ML"
    15 	  "Tools/res_types_sorts.ML"
    16 	  "Tools/res_atp.ML"
    17           "Tools/reconstruction.ML"
    18 
    19 begin
    20 
    21 text{*Every theory of HOL must be a descendant or ancestor of this one!*}
    22 
    23 setup Reconstruction.setup
    24 
    25 end