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)
paulson@15151
     1
(*  Title:      HOL/Reconstruction.thy
paulson@15151
     2
    ID: $Id$
paulson@15151
     3
    Author:     Lawrence C Paulson
paulson@15151
     4
    Copyright   2004  University of Cambridge
paulson@15151
     5
*)
paulson@15151
     6
paulson@15151
     7
header{*Attributes for Reconstructing External Resolution Proofs*}
paulson@15151
     8
paulson@15151
     9
theory Reconstruction
paulson@15382
    10
    imports Hilbert_Choice Map Infinite_Set
paulson@15359
    11
    files "Tools/res_lib.ML"
paulson@15359
    12
	  "Tools/res_clause.ML"
paulson@15359
    13
	  "Tools/res_skolem_function.ML"
paulson@15359
    14
	  "Tools/res_axioms.ML"
paulson@15359
    15
	  "Tools/res_types_sorts.ML"
paulson@15359
    16
	  "Tools/res_atp.ML"
paulson@15359
    17
          "Tools/reconstruction.ML"
paulson@15151
    18
paulson@15151
    19
begin
paulson@15151
    20
paulson@15382
    21
text{*Every theory of HOL must be a descendant or ancestor of this one!*}
paulson@15382
    22
paulson@15151
    23
setup Reconstruction.setup
paulson@15151
    24
paulson@15151
    25
end