--- a/src/HOL/Tools/ATP/SpassCommunication.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,4 +1,5 @@
(* Title: SpassCommunication.ml
+ ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
--- a/src/HOL/Tools/ATP/VampireCommunication.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/VampireCommunication.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,4 +1,5 @@
(* Title: VampireCommunication.ml
+ ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
--- a/src/HOL/Tools/ATP/modUnix.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/modUnix.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,3 +1,7 @@
+(* ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
(****************************************************************)
(****** Slightly modified version of sml Unix structure *********)
@@ -21,10 +25,10 @@
end
fun fdReader (name : string, fd : Posix.IO.file_desc) =
- Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
+ Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
fun fdWriter (name, fd) =
- Posix.IO.mkWriter {
+ Posix.IO.mkTextWriter {
appendMode = false,
initBlkMode = true,
name = name,
--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,3 +1,8 @@
+(* ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
(*----------------------------------------------*)
(* Reorder clauses for use in binary resolution *)
(*----------------------------------------------*)
--- a/src/HOL/Tools/ATP/recon_parse.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,3 +1,8 @@
+(* ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
(*use "Translate_Proof";*)
(* Parsing functions *)
--- a/src/HOL/Tools/ATP/recon_prelim.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_prelim.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,13 +1,7 @@
-
-
-Goal "A -->A";
-by Auto_tac;
-qed "foo";
-
-
-val Mainsign = #sign (rep_thm foo);
-
-
+(* ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
val gcounter = ref 0;
@@ -35,19 +29,6 @@
fun getstring (Var (v,T)) = fst v
|getstring (Free (v,T))= v;
-
-
-fun alltrue [] = true
- |alltrue (true::xs) = true andalso (alltrue xs)
- |alltrue (false::xs) = false;
-
-fun allfalse [] = true
- |allfalse (false::xs) = true andalso (allfalse xs)
- |allfalse (true::xs) = false;
-
-fun not_empty [] = false
- | not_empty _ = true;
-
fun twoisvar (a,b) = is_Var b;
fun twoisfree (a,b) = is_Free b;
fun twoiscomb (a,b) = iscomb b;
@@ -86,7 +67,7 @@
true
else
let val (f, args) = strip_comb t in
- if ((is_Free f) orelse (is_Var f)) andalso (alltrue (map is_hol_tm args)) then
+ if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then
true (* should be is_const *)
else
false
@@ -115,7 +96,7 @@
end
else if (iscomb f) then
let val (P, args) = strip_comb f in
- ((is_hol_tm P)) andalso (alltrue (map is_hol_fm args))
+ ((is_hol_tm P)) andalso (forall is_hol_fm args)
end
else
is_hol_tm f; (* should be is_const, nee
@@ -195,31 +176,9 @@
fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
-exception powerError;
-fun power (x, n) = if x = 0 andalso n = 0
- then raise powerError
- else if n = 0
- then 1
- else x * power (x, n-1);
-
-
-fun get_tens n = power(10, (n-1))
-
-
-fun digits_to_int [] posn n = n
-| digits_to_int (x::xs) posn n = let
- val digit_val = ((ord x) - 48)*(get_tens posn)
- in
- digits_to_int xs (posn -1 )(n + digit_val)
- end;
-
-fun int_of_string str = let
- val digits = explode str
- val posn = length digits
- in
- digits_to_int digits posn 0
- end
-
-
+fun int_of_string str = valOf (Int.fromString str)
+ handle Option => error ("int_of_string: " ^ str);
+
+
exception ASSERTION of string;
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,3 +1,8 @@
+(* ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
(******************)
(* complete later *)
(******************)
@@ -23,15 +28,6 @@
end
-fun thm_of_string str = let val _ = set show_sorts
- val term = read str
- val propterm = HOLogic.mk_Trueprop term
- val cterm = cterm_of Mainsign propterm
- val _ = reset show_sorts
- in
- assume cterm
- end
-
(* check separate args in the watcher program for separating strings with a * or ; or something *)
fun clause_strs_to_string [] str = str
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,4 +1,7 @@
-
+(* ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
fun add_in_order (x:string) [] = [x]
| add_in_order (x:string) ((y:string)::ys) = if (x < y)
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,3 +1,8 @@
+(* ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
(* Get claset rules *)
--- a/src/HOL/Tools/ATP/watcher.ML Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Thu Apr 21 15:05:24 2005 +0200
@@ -1,7 +1,7 @@
-
- (* Title: Watcher.ML
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
+(* Title: Watcher.ML
+ ID: $Id$
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
*)
(***************************************************************************)
--- a/src/HOL/Tools/ATP/watcher.sig Thu Apr 21 13:15:25 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.sig Thu Apr 21 15:05:24 2005 +0200
@@ -1,5 +1,4 @@
-
-(* Title: Watcher.ML
+(* ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
@@ -14,7 +13,7 @@
signature WATCHER =
- sig
+sig
(*****************************************************************************************)
(* Send request to Watcher for multiple spasses to be called for filenames in arg *)