Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Reconstruction.thy
changeset 16588 8de758143786
parent 16563 a92f96951355
child 17229 aca2ce40be35 
--- a/src/HOL/Reconstruction.thy	Tue Jun 28 15:27:45 2005 +0200
+++ b/src/HOL/Reconstruction.thy	Tue Jun 28 15:28:04 2005 +0200
@@ -9,25 +9,24 @@
 theory Reconstruction
     imports Hilbert_Choice Map Infinite_Set Extraction
     uses "Tools/res_lib.ML"
-	  "Tools/res_clause.ML"
-	  "Tools/res_skolem_function.ML"
-	  "Tools/res_axioms.ML"
-	  "Tools/res_types_sorts.ML"
+	 "Tools/res_clause.ML"
+	 "Tools/res_skolem_function.ML"
+	 "Tools/res_axioms.ML"
+	 "Tools/res_types_sorts.ML"
 
-      "Tools/ATP/recon_prelim.ML"
- 	  "Tools/ATP/recon_order_clauses.ML"
- 	  "Tools/ATP/recon_translate_proof.ML"
- 	  "Tools/ATP/recon_parse.ML"
- 	  "Tools/ATP/recon_transfer_proof.ML"
-	  "Tools/ATP/VampCommunication.ML"
-	  "Tools/ATP/VampireCommunication.ML"
-	  "Tools/ATP/SpassCommunication.ML"
-	  "Tools/ATP/watcher.sig"
-	  "Tools/ATP/watcher.ML"
-	  "Tools/ATP/res_clasimpset.ML"
-	  "Tools/res_atp.ML"
-
-      "Tools/reconstruction.ML"
+	 "Tools/ATP/recon_prelim.ML"
+	 "Tools/ATP/recon_order_clauses.ML"
+	 "Tools/ATP/recon_translate_proof.ML"
+	 "Tools/ATP/recon_parse.ML"
+	 "Tools/ATP/recon_transfer_proof.ML"
+	 "Tools/ATP/VampCommunication.ML"
+	 "Tools/ATP/VampireCommunication.ML"
+	 "Tools/ATP/SpassCommunication.ML"
+	 "Tools/ATP/watcher.sig"
+	 "Tools/ATP/watcher.ML"
+	 "Tools/ATP/res_clasimpset.ML"
+	 "Tools/res_atp.ML"
+	 "Tools/reconstruction.ML"
 
 begin
isabelle