src/HOL/Reconstruction.thy
author wenzelm
Thu, 22 Dec 2005 00:28:36 +0100
changeset 18457 356a9f711899
parent 18449 e314fb38307d
child 18794 46d66332bf81
permissions -rw-r--r--
structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Reconstruction.thy
17603
f601609d3300 spaces inserted in header
webertj
parents: 17508
diff changeset
     2
    ID:         $Id$
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     4
    Copyright   2004  University of Cambridge
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     5
*)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     6
17462
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents: 17421
diff changeset
     7
header{* Reconstructing external resolution proofs *}
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     8
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     9
theory Reconstruction
17508
c84af7f39a6b tuned theory dependencies;
wenzelm
parents: 17488
diff changeset
    10
imports Hilbert_Choice Map Infinite_Set Extraction
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents: 18004
diff changeset
    11
uses 	 "Tools/polyhash.ML"
e314fb38307d new hash table module in HOL/Too/s
paulson
parents: 18004
diff changeset
    12
         "Tools/res_clause.ML"
e314fb38307d new hash table module in HOL/Too/s
paulson
parents: 18004
diff changeset
    13
	 "Tools/res_hol_clause.ML"
17819
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    14
	 "Tools/res_axioms.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    15
	 "Tools/ATP/recon_order_clauses.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    16
	 "Tools/ATP/recon_translate_proof.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    17
	 "Tools/ATP/recon_parse.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    18
	 "Tools/ATP/recon_transfer_proof.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    19
	 "Tools/ATP/AtpCommunication.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    20
	 "Tools/ATP/watcher.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    21
	 "Tools/ATP/res_clasimpset.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    22
	 "Tools/res_atp.ML"
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17603
diff changeset
    23
	 "Tools/reconstruction.ML"
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    24
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    25
begin
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    26
16563
a92f96951355 meson method taking an argument list
paulson
parents: 16479
diff changeset
    27
setup ResAxioms.meson_method_setup
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    28
setup Reconstruction.setup
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    29
15653
3549ff7158f3 Updated to add watcher code.
quigley
parents: 15645
diff changeset
    30
end