--- a/contrib/SystemOnTPTP/remote Wed Jan 21 23:40:23 2009 +0100
+++ b/contrib/SystemOnTPTP/remote Wed Jan 21 23:42:37 2009 +0100
@@ -3,93 +3,137 @@
# Wrapper for custom remote provers on SystemOnTPTP
# Author: Fabian Immler, TU Muenchen
#
-# Similar to the vampire wrapper, but compatible provers can be passed in the
-# command line, with %s for the problemfile e.g.
-#
-# ./remote Vampire---9.0 jumpirefix --output_syntax tptp --mode casc -t 3600 %s
-# ./remote Vampire---10.0 drakosha.pl 60 %s
-# ./remote SPASS---3.01 SPASS -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof %s
-# ./remote Metis---2.1 metis --show proof --show saturation %s
-# ./remote SNARK---20080805r005 run-snark %s
use warnings;
use strict;
-
use Getopt::Std;
use HTTP::Request::Common;
-use LWP::UserAgent;
+use LWP;
-# address of proof-server
my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
-if(scalar(@ARGV) < 2) {
- print "prover and command missing";
- exit -1;
-}
-my $prover = shift(@ARGV);
-my $command = shift(@ARGV);
-
-# pass arguments
-my $options = "";
-while(scalar(@ARGV)>1){
- $options.=" ".shift(@ARGV);
-}
-# last argument is problemfile to be uploaded
-my $problem = [shift(@ARGV)];
-
-# fill in form
+# default parameters
my %URLParameters = (
"NoHTML" => 1,
"QuietFlag" => "-q01",
"X2TPTP" => "-S",
"SubmitButton" => "RunSelectedSystems",
"ProblemSource" => "UPLOAD",
- "UPLOADProblem" => $problem,
- "System___$prover" => "$prover",
- "Format___$prover" => "tptp",
- "Command___$prover" => "$command $options %s"
-);
+ );
+
+# check connection
+my $TestAgent = LWP::UserAgent->new;
+$TestAgent->timeout(5);
+my $TestRequest = GET($SystemOnTPTPFormReplyURL);
+my $TestResponse = $TestAgent->request($TestRequest);
+if(! $TestResponse->is_success) {
+ print "HTTP-Error: " . $TestResponse->message . "\n";
+ exit(-1);
+}
+
+#----Get format and transform options if specified
+my %Options;
+getopts("hws:t:c:",\%Options);
+
+#----Usage
+if (exists($Options{'h'})) {
+ print("Usage: remote <options> [<File name>]\n");
+ print(" <options> are ...\n");
+ print(" -h - print this help\n");
+ print(" -w - list available ATP systems\n");
+ print(" -s<system> - specified system to use\n");
+ print(" -t<timelimit> - CPU time limit for system\n");
+ print(" -c<command> - custom command for system\n");
+ print(" <File name> - TPTP problem file\n");
+ exit(0);
+}
+
+#----What systems flag
+if (exists($Options{'w'})) {
+ $URLParameters{"SubmitButton"} = "ListSystems";
+ delete($URLParameters{"ProblemSource"});
+}
+#----Selected system
+my $System;
+if (exists($Options{'s'})) {
+ $System = $Options{'s'};
+} else {
+ # use Vampire as default
+ $System = "Vampire---9.0";
+}
+$URLParameters{"System___$System"} = $System;
+
+#----Time limit
+if (exists($Options{'t'})) {
+ $URLParameters{"TimeLimit___$System"} = $Options{'t'};
+}
+#----Custom command
+if (exists($Options{'c'})) {
+ $URLParameters{"Command___$System"} = $Options{'c'};
+}
+
+#----Get single file name
+if (exists($URLParameters{"ProblemSource"})) {
+ if (scalar(@ARGV) >= 1) {
+ $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
+ } else {
+die("Missing problem file");
+ }
+}
# Query Server
my $Agent = LWP::UserAgent->new;
+if (exists($Options{'t'})) {
+ # give server more time to respond
+ $Agent->timeout($Options{'t'} * 2 + 10);
+}
my $Request = POST($SystemOnTPTPFormReplyURL,
Content_Type => 'form-data',Content => \%URLParameters);
my $Response = $Agent->request($Request);
-
-#catch errors, let isabelle/watcher know
-if($Response->is_success && $Response->content !~ /NO SOLUTION OUTPUT BY SYSTEM/
-&& $Response->content =~ m/%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/){
- # convert to isabelle-friendly format
- my @lines = split( /%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/, $Response->content);
- @lines = split( /\n/, $lines[1]); my $extract = "";
- my $inproof = 0 > 1;
- my $ende = 0 > 1;
+
+#catch errors / failure
+if(! $Response->is_success){
+ print "HTTP-Error: " . $Response->message . "\n";
+ exit(-1);
+} elsif (exists($Options{'w'})) {
+ print $Response->content;
+ exit (0);
+} elsif ($Response->content =~ /NO SOLUTION OUTPUT BY SYSTEM/){
+ if ($Response->content =~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
+ print "No Solution Output\nResult: $1\nOutput: $2\n";
+ } else {
+ print "No Solution Output\n";
+ }
+ exit(-1);
+} elsif ($Response->content =~ /ERROR: Could not form TPTP format derivation/) {
+ print "Could not form TPTP format derivation\n";
+ exit(-1);
+} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
+ print "Specified System $1 does not exist\n";
+ exit(-1);
+} elsif ($Response->content =~ /^\s*$/) {
+ print "Empty response (specified bad system? Inappropriate problem file format?)\n";
+ exit(-1);
+} elsif ($Response->content !~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
+ print "Bad response: \n".$Response->content;
+ exit(-1);
+} else {
+ my @lines = split( /\n/, $Response->content);
+ my $extract = "";
foreach my $line (@lines){
- if(! $ende){
- #ignore comments
- if(! $inproof){
- if ($line !~ /^%/ && !($line eq "")) {
- $extract .= "$line";
- $inproof = 1;
- }
- } else {
- if ($line !~ /^%/) {
- $extract .= "$line";
- } else {
- $ende = 1;
- }
- }
+ #ignore comments
+ if ($line !~ /^%/ && !($line eq "")) {
+ $extract .= "$line";
}
}
- # insert newlines after '.'
+ # insert newlines after ').'
$extract =~ s/\s//g;
$extract =~ s/\)\.cnf/\)\.\ncnf/g;
+
+ # orientation for res_reconstruct.ML
print "# SZS output start CNFRefutation.\n";
print "$extract\n";
print "# SZS output end CNFRefutation.\n";
-} else {
- print "HTTP-Request: " . $Response->message;
- print "\nCANNOT PROVE: \n";
- print $Response->content;
+ exit(0);
}
--- a/contrib/SystemOnTPTP/vampire Wed Jan 21 23:40:23 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-#!/usr/bin/env perl
-#
-# Vampire Wrapper for SystemOnTPTP
-# Author: Fabian Immler, TU Muenchen
-#
-# - querys a Vampire theorem prover on SystemOnTPTP
-# (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)
-# - behaves like a local Vampire
-# => can be used for Isabelle when Vampire is not available (e.g. on a Mac)
-#
-
-use warnings;
-use strict;
-
-use Getopt::Std;
-use HTTP::Request::Common;
-use LWP::UserAgent;
-
-# address of proof-server
-my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
-
-#name of prover and its executable on the server, e.g.
-# Vampire---9.0
-# jumpirefix
-my $prover = "Vampire---9.0";
-my $command = "jumpirefix";
-
-# pass arguments
-my $options = "";
-while(scalar(@ARGV)>1){
- $options.=" ".shift(@ARGV);
-}
-# last argument is problemfile to be uploaded
-my $problem = [shift(@ARGV)];
-
-# fill in form
-my %URLParameters = (
- "NoHTML" => 1,
- "QuietFlag" => "-q01",
- "SubmitButton" => "RunSelectedSystems",
- "ProblemSource" => "UPLOAD",
- "UPLOADProblem" => $problem,
- "System___$prover" => "$prover",
- "Format___$prover" => "tptp",
- "Command___$prover" => "$command $options %s"
-);
-
-# Query Server
-my $Agent = LWP::UserAgent->new;
-my $Request = POST($SystemOnTPTPFormReplyURL,
- Content_Type => 'form-data',Content => \%URLParameters);
-my $Response = $Agent->request($Request);
-
-#catch errors, let isabelle/watcher know
-if($Response->is_success){
- print $Response->content;
-} else {
- print $Response->message;
- print "\nCANNOT PROVE\n";
-}
--- a/etc/isar-keywords-ZF.el Wed Jan 21 23:40:23 2009 +0100
+++ b/etc/isar-keywords-ZF.el Wed Jan 21 23:42:37 2009 +0100
@@ -3,14 +3,16 @@
;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
-;; $Id$
-;;
(defconst isar-keywords-major
'("\\."
"\\.\\."
"Isabelle\\.command"
+ "Isar\\.begin_document"
"Isar\\.command"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
"Isar\\.insert"
"Isar\\.remove"
"ML"
@@ -89,7 +91,6 @@
"instantiation"
"interpret"
"interpretation"
- "invoke"
"judgment"
"kill"
"kill_thy"
@@ -135,7 +136,6 @@
"print_drafts"
"print_facts"
"print_induct_rules"
- "print_interps"
"print_locale"
"print_locales"
"print_methods"
@@ -249,7 +249,11 @@
(defconst isar-keywords-control
'("Isabelle\\.command"
+ "Isar\\.begin_document"
"Isar\\.command"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
"Isar\\.insert"
"Isar\\.remove"
"ProofGeneral\\.inform_file_processed"
@@ -298,7 +302,6 @@
"print_drafts"
"print_facts"
"print_induct_rules"
- "print_interps"
"print_locale"
"print_locales"
"print_methods"
@@ -438,8 +441,7 @@
(defconst isar-keywords-proof-goal
'("have"
"hence"
- "interpret"
- "invoke"))
+ "interpret"))
(defconst isar-keywords-proof-block
'("next"
--- a/etc/isar-keywords.el Wed Jan 21 23:40:23 2009 +0100
+++ b/etc/isar-keywords.el Wed Jan 21 23:42:37 2009 +0100
@@ -3,14 +3,16 @@
;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
-;; $Id$
-;;
(defconst isar-keywords-major
'("\\."
"\\.\\."
"Isabelle\\.command"
+ "Isar\\.begin_document"
"Isar\\.command"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
"Isar\\.insert"
"Isar\\.remove"
"ML"
@@ -46,9 +48,6 @@
"chapter"
"class"
"class_deps"
- "class_interpret"
- "class_interpretation"
- "class_locale"
"classes"
"classrel"
"code_abort"
@@ -119,7 +118,6 @@
"instantiation"
"interpret"
"interpretation"
- "invoke"
"judgment"
"kill"
"kill_thy"
@@ -172,7 +170,6 @@
"print_drafts"
"print_facts"
"print_induct_rules"
- "print_interps"
"print_locale"
"print_locales"
"print_methods"
@@ -312,7 +309,11 @@
(defconst isar-keywords-control
'("Isabelle\\.command"
+ "Isar\\.begin_document"
"Isar\\.command"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
"Isar\\.insert"
"Isar\\.remove"
"ProofGeneral\\.inform_file_processed"
@@ -369,7 +370,6 @@
"print_drafts"
"print_facts"
"print_induct_rules"
- "print_interps"
"print_locale"
"print_locales"
"print_methods"
@@ -423,7 +423,6 @@
"axiomatization"
"axioms"
"class"
- "class_locale"
"classes"
"classrel"
"code_abort"
@@ -507,7 +506,6 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
- "class_interpretation"
"corollary"
"cpodef"
"function"
@@ -546,11 +544,9 @@
"subsubsect"))
(defconst isar-keywords-proof-goal
- '("class_interpret"
- "have"
+ '("have"
"hence"
- "interpret"
- "invoke"))
+ "interpret"))
(defconst isar-keywords-proof-block
'("next"
--- a/etc/settings Wed Jan 21 23:40:23 2009 +0100
+++ b/etc/settings Wed Jan 21 23:42:37 2009 +0100
@@ -242,7 +242,6 @@
"$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
"$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
"/usr/local/Vampire" \
- "$ISABELLE_HOME/contrib/SystemOnTPTP" \
"")
SPASS_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
--- a/lib/jedit/isabelle.xml Wed Jan 21 23:40:23 2009 +0100
+++ b/lib/jedit/isabelle.xml Wed Jan 21 23:42:37 2009 +0100
@@ -2,7 +2,6 @@
<!DOCTYPE MODE SYSTEM "xmode.dtd">
<!-- Generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + FOL + ZF. -->
<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->
-<!-- $Id$ -->
<MODE>
<PROPS>
<PROPERTY NAME="commentStart" VALUE="(*"/>
@@ -36,7 +35,11 @@
<OPERATOR>.</OPERATOR>
<OPERATOR>..</OPERATOR>
<INVALID>Isabelle.command</INVALID>
+ <INVALID>Isar.begin_document</INVALID>
<INVALID>Isar.command</INVALID>
+ <INVALID>Isar.define_command</INVALID>
+ <INVALID>Isar.edit_document</INVALID>
+ <INVALID>Isar.end_document</INVALID>
<INVALID>Isar.insert</INVALID>
<INVALID>Isar.remove</INVALID>
<OPERATOR>ML</OPERATOR>
@@ -171,7 +174,6 @@
<OPERATOR>interpret</OPERATOR>
<OPERATOR>interpretation</OPERATOR>
<KEYWORD4>intros</KEYWORD4>
- <OPERATOR>invoke</OPERATOR>
<KEYWORD4>is</KEYWORD4>
<OPERATOR>judgment</OPERATOR>
<INVALID>kill</INVALID>
@@ -239,7 +241,6 @@
<LABEL>print_drafts</LABEL>
<LABEL>print_facts</LABEL>
<LABEL>print_induct_rules</LABEL>
- <LABEL>print_interps</LABEL>
<LABEL>print_locale</LABEL>
<LABEL>print_locales</LABEL>
<LABEL>print_methods</LABEL>
--- a/src/HOL/ATP_Linkup.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy Wed Jan 21 23:42:37 2009 +0100
@@ -111,10 +111,13 @@
setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_opts 40 false) *}
text {* remote provers via SystemOnTPTP *}
-setup {* AtpManager.add_prover "remote_vamp9"
- (AtpWrapper.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
-setup {* AtpManager.add_prover "remote_vamp10"
- (AtpWrapper.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
+setup {* AtpManager.add_prover "remote_vampire"
+ (AtpWrapper.remote_prover "-s Vampire---9.0") *}
+setup {* AtpManager.add_prover "remote_spass"
+ (AtpWrapper.remote_prover "-s SPASS---3.01") *}
+setup {* AtpManager.add_prover "remote_e"
+ (AtpWrapper.remote_prover "-s EP---1.0") *}
+
subsection {* The Metis prover *}
--- a/src/HOL/Tools/atp_manager.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Tools/atp_manager.ML Wed Jan 21 23:42:37 2009 +0100
@@ -19,7 +19,7 @@
val kill: unit -> unit
val info: unit -> unit
val messages: int option -> unit
- type prover = int -> Proof.state -> bool * string
+ type prover = int -> int -> Proof.state -> bool * string
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
val sledgehammer: string list -> Proof.state -> unit
@@ -35,9 +35,9 @@
local
-val atps = ref "e";
+val atps = ref "e remote_vampire";
val max_atps = ref 5; (* ~1 means infinite number of atps *)
-val timeout = ref 60;
+val timeout = ref 100;
in
@@ -114,16 +114,18 @@
val (group, active') =
if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
else List.partition (fn (th, _) => Thread.equal (th, thread)) active
- val others = delete_thread thread group
+ (* do not interrupt successful thread, as it needs to print out its message
+ (and terminates afterwards - see start_prover )*)
+ val group' = if success then delete_thread thread group else group
val now = Time.now ()
val cancelling' =
- fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) others cancelling
+ fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group' cancelling
val msg = description ^ "\n" ^ message
val message' = "Sledgehammer: " ^ msg ^
- (if null others then ""
- else "\nInterrupted " ^ string_of_int (length others) ^ " other group members")
+ (if length group <= 1 then ""
+ else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members")
val messages' = msg ::
(if length messages <= message_store_limit then messages
else #1 (chop message_store_limit messages))
@@ -264,7 +266,7 @@
(* named provers *)
-type prover = int -> Proof.state -> bool * string;
+type prover = int -> int -> Proof.state -> bool * string;
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
@@ -300,7 +302,7 @@
val _ = SimpleThread.fork true (fn () =>
let
val _ = register birthtime deadtime (Thread.self (), desc)
- val result = prover i proof_state
+ val result = prover (get_timeout ()) i proof_state
handle ResHolClause.TOO_TRIVIAL
=> (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg
--- a/src/HOL/Tools/atp_wrapper.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML Wed Jan 21 23:42:37 2009 +0100
@@ -12,7 +12,7 @@
val external_prover:
((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
Path.T * string ->
- (string * int -> bool) ->
+ (string -> string option) ->
(string * string vector * Proof.context * thm * int -> string) ->
AtpManager.prover
val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
@@ -30,8 +30,8 @@
val eprover_full: AtpManager.prover
val spass_opts: int -> bool -> AtpManager.prover
val spass: AtpManager.prover
- val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
- val remote_prover: string -> string -> AtpManager.prover
+ val remote_prover_opts: int -> bool -> string -> AtpManager.prover
+ val remote_prover: string -> AtpManager.prover
end;
structure AtpWrapper: ATP_WRAPPER =
@@ -47,7 +47,7 @@
(* basic template *)
-fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
+fun external_prover write_problem_files (cmd, args) find_failure produce_answer timeout subgoalno state =
let
(* path to unique problem file *)
val destdir' = ! destdir
@@ -70,19 +70,18 @@
if File.exists cmd then File.shell_path cmd ^ " " ^ args
else error ("Bad executable: " ^ Path.implode cmd)
val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1))
- val _ =
- if rc <> 0 then
- warning ("Sledgehammer prover exited with return code " ^ string_of_int rc ^ "\n" ^ cmdline)
- else ()
(* remove *temporary* files *)
val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else ()
-
- val success = check_success (proof, rc)
+
+ (* check for success and print out some information on failure *)
+ val failure = find_failure proof
+ val success = rc = 0 andalso is_none failure
val message =
- if success
- then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
- else "Failed."
+ if isSome failure then "Could not prove: " ^ the failure
+ else if rc <> 0
+ then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof
+ else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
in (success, message) end;
@@ -95,7 +94,7 @@
external_prover
(ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
command
- ResReconstruct.check_success_e_vamp_spass
+ ResReconstruct.find_failure_e_vamp_spass
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
@@ -115,15 +114,19 @@
(*NB: Vampire does not work without explicit timelimit*)
-fun vampire_opts max_new theory_const = tptp_prover_opts
+fun vampire_opts max_new theory_const timeout = tptp_prover_opts
max_new theory_const
- (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600");
+ (Path.explode "$VAMPIRE_HOME/vampire",
+ ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+ timeout;
val vampire = vampire_opts 60 false;
-fun vampire_opts_full max_new theory_const = full_prover_opts
+fun vampire_opts_full max_new theory_const timeout = full_prover_opts
max_new theory_const
- (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600");
+ (Path.explode "$VAMPIRE_HOME/vampire",
+ ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+ timeout;
val vampire_full = vampire_opts 60 false;
@@ -148,7 +151,7 @@
fun spass_opts max_new theory_const = external_prover
(ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
(Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
- ResReconstruct.check_success_e_vamp_spass
+ ResReconstruct.find_failure_e_vamp_spass
ResReconstruct.lemma_list_dfg;
val spass = spass_opts 40 true;
@@ -156,9 +159,10 @@
(* remote prover invocation via SystemOnTPTP *)
-fun remote_prover_opts max_new theory_const name command =
+fun remote_prover_opts max_new theory_const args timeout =
tptp_prover_opts max_new theory_const
- (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command);
+ (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout)
+ timeout;
val remote_prover = remote_prover_opts 60 false;
--- a/src/HOL/Tools/res_reconstruct.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Wed Jan 21 23:42:37 2009 +0100
@@ -15,7 +15,7 @@
val strip_prefix: string -> string -> string option
val setup: Context.theory -> Context.theory
(* extracting lemma list*)
- val check_success_e_vamp_spass: string * int -> bool
+ val find_failure_e_vamp_spass: string -> string option
val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string
val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string
(* structured proofs *)
@@ -463,11 +463,12 @@
val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.",
"SPASS beiseite: Maximal number of loops exceeded."];
- fun check_success_e_vamp_spass (proof, rc) =
- not (exists (fn s => String.isSubstring s proof)
- (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS))
- andalso (rc = 0);
-
+ fun find_failure_e_vamp_spass proof =
+ let val failures =
+ map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
+ (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS)
+ in if null failures then NONE else SOME (hd failures) end;
+
(*=== EXTRACTING PROOF-TEXT === *)
val begin_proof_strings = ["# SZS output start CNFRefutation.",
--- a/src/Pure/General/ROOT.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/ROOT.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/ROOT.ML
- ID: $Id$
Library of general tools.
*)
--- a/src/Pure/General/alist.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/alist.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/alist.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Association lists -- lists of (key, value) pairs.
--- a/src/Pure/General/balanced_tree.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/balanced_tree.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/balanced_tree.ML
- ID: $Id$
Author: Lawrence C Paulson and Makarius
Balanced binary trees.
--- a/src/Pure/General/basics.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/basics.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/basics.ML
- ID: $Id$
Author: Florian Haftmann and Makarius, TU Muenchen
Fundamental concepts.
--- a/src/Pure/General/file.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/file.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/file.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
File system operations.
--- a/src/Pure/General/graph.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/graph.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/graph.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Directed graphs.
--- a/src/Pure/General/heap.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/heap.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,6 +1,5 @@
(* Title: Pure/General/heap.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
+ Author: Lawrence C Paulson and Markus Wenzel
Heaps over linearly ordered types. See also Chris Okasaki: "Purely
Functional Data Structures" (Chapter 3), Cambridge University Press,
--- a/src/Pure/General/integer.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/integer.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/integer.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Unbounded integers.
--- a/src/Pure/General/ord_list.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/ord_list.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/ord_list.ML
- ID: $Id$
Author: Makarius
Ordered lists without duplicates -- a light-weight representation of
--- a/src/Pure/General/output.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/output.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/output.ML
- ID: $Id$
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
Output channels and timing messages.
--- a/src/Pure/General/path.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/path.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/path.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Abstract algebra of file paths (external encoding in Unix style).
--- a/src/Pure/General/pretty.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/pretty.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/pretty.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Markus Wenzel, TU Munich
--- a/src/Pure/General/print_mode.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/print_mode.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/print_mode.ML
- ID: $Id$
Author: Makarius
Generic print mode as thread-local value derived from global template;
--- a/src/Pure/General/properties.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/properties.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/properties.ML
- ID: $Id$
Author: Makarius
Property lists.
--- a/src/Pure/General/queue.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/queue.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/queue.ML
- ID: $Id$
Author: Makarius
Efficient queues.
--- a/src/Pure/General/scan.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/scan.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/scan.ML
- ID: $Id$
Author: Markus Wenzel and Tobias Nipkow, TU Muenchen
Generic scanners (for potentially infinite input).
--- a/src/Pure/General/secure.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/secure.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/secure.ML
- ID: $Id$
Author: Makarius
Secure critical operations.
--- a/src/Pure/General/seq.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/seq.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/seq.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Markus Wenzel, TU Munich
--- a/src/Pure/General/source.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/source.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/source.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Coalgebraic data sources -- efficient purely functional input streams.
--- a/src/Pure/General/stack.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/stack.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/stack.ML
- ID: $Id$
Author: Makarius
Non-empty stacks.
--- a/src/Pure/General/symbol.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/symbol.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/symbol.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Generalized characters with infinitely many named symbols.
--- a/src/Pure/General/symbol_pos.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/symbol_pos.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/symbol_pos.ML
- ID: $Id$
Author: Makarius
Symbols with explicit position information.
--- a/src/Pure/General/table.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/table.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/table.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Generic tables. Efficient purely functional implementation using
--- a/src/Pure/General/url.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/url.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/url.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Basic URLs, see RFC 1738 and RFC 2396.
--- a/src/Pure/General/xml.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/xml.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/xml.ML
- ID: $Id$
Author: David Aspinall, Stefan Berghofer and Markus Wenzel
Basic support for XML.
--- a/src/Pure/General/yxml.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/General/yxml.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/yxml.ML
- ID: $Id$
Author: Makarius
Efficient text representation of XML trees using extra characters X
--- a/src/Pure/Isar/antiquote.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/antiquote.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/antiquote.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Text with antiquotations of inner items (terms, types etc.).
--- a/src/Pure/Isar/args.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/args.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/args.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Parsing with implicit value assigment. Concrete argument syntax of
--- a/src/Pure/Isar/auto_bind.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/auto_bind.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/auto_bind.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Automatic bindings of Isar text elements.
--- a/src/Pure/Isar/calculation.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/calculation.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Generic calculational proofs.
--- a/src/Pure/Isar/context_rules.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/context_rules.ML
- ID: $Id$
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
Declarations of intro/elim/dest rules in Pure (see also
--- a/src/Pure/Isar/element.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/element.ML Wed Jan 21 23:42:37 2009 +0100
@@ -23,20 +23,12 @@
val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
(Attrib.binding * ('fact * Attrib.src list) list) list ->
(Attrib.binding * ('c * Attrib.src list) list) list
- val map_ctxt': {binding: binding -> binding,
- var: binding * mixfix -> binding * mixfix,
- typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c,
- attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
- val map_ctxt: {binding: binding -> binding,
- var: binding * mixfix -> binding * mixfix,
- typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
- attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
+ val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
+ pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} ->
+ ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
val morph_ctxt: morphism -> context_i -> context_i
- val params_of: context_i -> (string * typ) list
- val prems_of: context_i -> term list
- val facts_of: theory -> context_i -> (Attrib.binding * (thm list * Attrib.src list) list) list
val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
val pretty_statement: Proof.context -> string -> thm -> Pretty.T
@@ -51,14 +43,6 @@
val morph_witness: morphism -> witness -> witness
val conclude_witness: witness -> thm
val pretty_witness: Proof.context -> witness -> Pretty.T
- val rename: (string * (string * mixfix option)) list -> string -> string
- val rename_var_name: (string * (string * mixfix option)) list ->
- string * mixfix -> string * mixfix
- val rename_var: (string * (string * mixfix option)) list ->
- binding * mixfix -> binding * mixfix
- val rename_term: (string * (string * mixfix option)) list -> term -> term
- val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
- val rename_morphism: (string * (string * mixfix option)) list -> morphism
val instT_type: typ Symtab.table -> typ -> typ
val instT_term: typ Symtab.table -> term -> term
val instT_thm: theory -> typ Symtab.table -> thm -> thm
@@ -109,53 +93,29 @@
fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
-fun map_ctxt' {binding, var, typ, term, pat, fact, attrib} =
- fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
- let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
+fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
+ fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
| Constrains xs => Constrains (xs |> map (fn (x, T) =>
- let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
+ (Binding.base_name (binding (Binding.name x)), typ T)))
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
- ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pat ps)))))
+ ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
- ((binding a, map attrib atts), (term t, map pat ps))))
+ ((binding a, map attrib atts), (term t, map pattern ps))))
| Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
-fun map_ctxt {binding, var, typ, term, fact, attrib} =
- map_ctxt' {binding = binding, var = var, typ = typ, term = term, pat = term,
- fact = fact, attrib = attrib}
-
fun map_ctxt_attrib attrib =
- map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
+ map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
fun morph_ctxt phi = map_ctxt
{binding = Morphism.binding phi,
- var = Morphism.var phi,
typ = Morphism.typ phi,
term = Morphism.term phi,
+ pattern = Morphism.term phi,
fact = Morphism.fact phi,
attrib = Args.morph_values phi};
-(* logical content *)
-
-fun params_of (Fixes fixes) = fixes |> map
- (fn (x, SOME T, _) => (Binding.base_name x, T)
- | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), []))
- | params_of _ = [];
-
-fun prems_of (Assumes asms) = maps (map fst o snd) asms
- | prems_of (Defines defs) = map (fst o snd) defs
- | prems_of _ = [];
-
-fun assume thy t = Assumption.assume (Thm.cterm_of thy t);
-
-fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms
- | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs
- | facts_of _ (Notes (_, facts)) = facts
- | facts_of _ _ = [];
-
-
(** pretty printing **)
@@ -165,9 +125,8 @@
map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
fun pretty_name_atts ctxt (b, atts) sep =
- let
- val name = Binding.display b;
- in if name = "" andalso null atts then []
+ let val name = Binding.display b in
+ if name = "" andalso null atts then []
else [Pretty.block
(Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
end;
@@ -307,6 +266,7 @@
Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
Tactic.rtac Drule.protectI 1 THEN tac)));
+
local
val refine_witness =
@@ -320,8 +280,7 @@
val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss
@ [map (rpair []) eq_props];
fun after_qed' thmss =
- let
- val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
+ let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness #> Seq.hd end;
@@ -340,7 +299,8 @@
cmd NONE after_qed' (map (pair (Binding.empty, [])) propss))
(fn wits => fn _ => after_qed wits) wit_propss [];
-end; (*local*)
+end;
+
fun compose_witness (Witness (_, th)) r =
let
@@ -398,50 +358,6 @@
end;
-(* rename *)
-
-fun rename ren x =
- (case AList.lookup (op =) ren (x: string) of
- NONE => x
- | SOME (x', _) => x');
-
-fun rename_var_name ren (x, mx) =
- (case (AList.lookup (op =) ren x, mx) of
- (NONE, _) => (x, mx)
- | (SOME (x', NONE), Structure) => (x', mx)
- | (SOME (x', SOME _), Structure) =>
- error ("Attempt to change syntax of structure parameter " ^ quote x)
- | (SOME (x', NONE), _) => (x', NoSyn)
- | (SOME (x', SOME mx'), _) => (x', mx'));
-
-fun rename_var ren (b, mx) =
- let
- val x = Binding.base_name b;
- val (x', mx') = rename_var_name ren (x, mx);
- in (Binding.name x', mx') end;
-
-fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
- | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
- | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
- | rename_term _ a = a;
-
-fun rename_thm ren th =
- let
- val thy = Thm.theory_of_thm th;
- val subst = (Thm.fold_terms o Term.fold_aterms)
- (fn Free (x, T) =>
- let val x' = rename ren x
- in if x = x' then I else insert (eq_fst (op =)) ((x, T), Free (x', T)) end
- | _ => I) th [];
- in
- if null subst then th
- else th |> hyps_rule (instantiate_frees thy subst)
- end;
-
-fun rename_morphism ren = Morphism.morphism
- {binding = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)};
-
-
(* instantiate types *)
fun instT_type env =
@@ -467,7 +383,7 @@
fun instT_morphism thy env =
let val thy_ref = Theory.check_thy thy in
Morphism.morphism
- {binding = I, var = I,
+ {binding = I,
typ = instT_type env,
term = instT_term env,
fact = map (fn th => instT_thm (Theory.deref thy_ref) env th)}
@@ -516,7 +432,7 @@
fun inst_morphism thy envs =
let val thy_ref = Theory.check_thy thy in
Morphism.morphism
- {binding = I, var = I,
+ {binding = I,
typ = instT_type (#1 envs),
term = inst_term envs,
fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)}
@@ -530,15 +446,15 @@
NONE => I
| SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
-fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns);
-
-fun satisfy_facts witns = facts_map (morph_ctxt (satisfy_morphism witns));
+val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
+val satisfy_facts = facts_map o morph_ctxt o satisfy_morphism;
(* rewriting with equalities *)
fun eq_morphism thy thms = Morphism.morphism
- {binding = I, var = I, typ = I,
+ {binding = I,
+ typ = I,
term = MetaSimplifier.rewrite_term thy thms [],
fact = map (MetaSimplifier.rewrite_rule thms)};
@@ -555,18 +471,16 @@
val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer;
val exp_term = Drule.term_rule thy (singleton exp_fact);
val exp_typ = Logic.type_map exp_term;
- val morphism =
- Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
+ val morphism = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
in facts_map (morph_ctxt morphism) facts end;
(* transfer to theory using closure *)
fun transfer_morphism thy =
- let val thy_ref = Theory.check_thy thy in
- Morphism.morphism {binding = I, var = I, typ = I, term = I,
- fact = map (fn th => transfer (Theory.deref thy_ref) th)}
- end;
+ let val thy_ref = Theory.check_thy thy
+ in Morphism.thm_morphism (fn th => transfer (Theory.deref thy_ref) th) end;
+
(** activate in context, return elements and facts **)
@@ -613,11 +527,14 @@
if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
else name;
-fun prep_facts prep_name get intern ctxt elem = elem |> map_ctxt
- {var = I, typ = I, term = I,
- binding = Binding.map_base prep_name,
- fact = get ctxt,
- attrib = intern (ProofContext.theory_of ctxt)};
+fun prep_facts prep_name get intern ctxt =
+ map_ctxt
+ {binding = Binding.map_base prep_name,
+ typ = I,
+ term = I,
+ pattern = I,
+ fact = get ctxt,
+ attrib = intern (ProofContext.theory_of ctxt)};
in
--- a/src/Pure/Isar/expression.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/expression.ML Wed Jan 21 23:42:37 2009 +0100
@@ -198,11 +198,14 @@
(** Parsing **)
-fun parse_elem prep_typ prep_term ctxt elem =
- Element.map_ctxt' {binding = I, var = I, typ = prep_typ ctxt,
- term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt), (* FIXME ?? *)
- pat = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
- fact = I, attrib = I} elem;
+fun parse_elem prep_typ prep_term ctxt =
+ Element.map_ctxt
+ {binding = I,
+ typ = prep_typ ctxt,
+ term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt),
+ pattern = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
+ fact = I,
+ attrib = I};
fun parse_concl prep_term ctxt concl =
(map o map) (fn (t, ps) =>
@@ -490,8 +493,7 @@
val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
val exp_typ = Logic.type_map exp_term;
- val export' =
- Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
+ val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
in ((propss, deps, export'), goal_ctxt) end;
in
--- a/src/Pure/Isar/local_syntax.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/local_syntax.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/local_syntax.ML
- ID: $Id$
Author: Makarius
Local syntax depending on theory syntax.
--- a/src/Pure/Isar/net_rules.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/net_rules.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/net_rules.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Efficient storage of rules: preserves order, prefers later entries.
--- a/src/Pure/Isar/object_logic.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/object_logic.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Specifics about common object-logics.
--- a/src/Pure/Isar/outer_lex.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/outer_lex.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/outer_lex.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Outer lexical syntax for Isabelle/Isar.
--- a/src/Pure/Isar/overloading.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/overloading.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/overloading.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Overloaded definitions without any discipline.
--- a/src/Pure/Isar/proof_context.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/proof_context.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
The key concept of Isar proof contexts: elevates primitive local
--- a/src/Pure/Isar/proof_display.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/proof_display.ML
- ID: $Id$
Author: Makarius
Printing of theorems, goals, results etc.
--- a/src/Pure/Isar/proof_node.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/proof_node.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/proof_node.ML
- ID: $Id$
Author: Makarius
Proof nodes with linear position and backtracking.
--- a/src/Pure/Isar/rule_insts.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/rule_insts.ML
- ID: $Id$
Author: Makarius
Rule instantiations -- operations within a rule/subgoal context.
--- a/src/Pure/Isar/skip_proof.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/skip_proof.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/skip_proof.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Skipping proofs -- quick_and_dirty mode.
--- a/src/Pure/Isar/spec_parse.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML Wed Jan 21 23:42:37 2009 +0100
@@ -24,7 +24,7 @@
val locale_fixes: (binding * string option * mixfix) list parser
val locale_insts: (string option list * (Attrib.binding * string) list) parser
val class_expr: string list parser
- val locale_expression: Expression.expression parser
+ val locale_expression: Expression.expression parser
val locale_keyword: string parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
--- a/src/Pure/Isar/specification.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/specification.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/specification.ML
- ID: $Id$
Author: Makarius
Derived local theory specifications --- with type-inference and
--- a/src/Pure/ML/ml_antiquote.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_antiquote.ML
- ID: $Id$
Author: Makarius
Common ML antiquotations.
--- a/src/Pure/ML/ml_context.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_context.ML
- ID: $Id$
Author: Makarius
ML context and antiquotations.
--- a/src/Pure/ML/ml_lex.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_lex.ML
- ID: $Id$
Author: Makarius
Lexical syntax for SML.
--- a/src/Pure/ML/ml_parse.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_parse.ML
- ID: $Id$
Author: Makarius
Minimal parsing for SML -- fixing integer numerals.
--- a/src/Pure/ML/ml_syntax.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ML/ml_syntax.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_syntax.ML
- ID: $Id$
Author: Makarius
Basic ML syntax operations.
--- a/src/Pure/ML/ml_thms.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ML/ml_thms.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML/ml_thms.ML
- ID: $Id$
Author: Makarius
Isar theorem values within ML.
--- a/src/Pure/Proof/proof_syntax.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Proof/proof_syntax.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Function for parsing and printing proof terms.
--- a/src/Pure/ProofGeneral/ROOT.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/ROOT.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/ROOT.ML
- ID: $Id$
Author: David Aspinall
Proof General interface for Isabelle, both the traditional Emacs version,
--- a/src/Pure/ProofGeneral/pgip.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip.ML
- ID: $Id$
Author: David Aspinall
Prover-side PGIP abstraction.
--- a/src/Pure/ProofGeneral/pgip_input.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_input.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_input.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: input commands.
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_isabelle.ML
- ID: $Id$
Author: David Aspinall
Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
--- a/src/Pure/ProofGeneral/pgip_markup.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_markup.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_markup.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: document markup for proof scripts (in progress).
--- a/src/Pure/ProofGeneral/pgip_output.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_output.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_output.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: output commands.
--- a/src/Pure/ProofGeneral/pgip_parser.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_parser.ML
- ID: $Id$
Author: David Aspinall and Makarius
Parsing theory sources without execution (via keyword classification).
--- a/src/Pure/ProofGeneral/pgip_tests.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_tests.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_tests.ML
- ID: $Id$
Author: David Aspinall
A test suite for the PGIP abstraction code (in progress).
--- a/src/Pure/ProofGeneral/pgip_types.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgip_types.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: types and conversions.
--- a/src/Pure/ProofGeneral/pgml.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/pgml.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/pgml.ML
- ID: $Id$
Author: David Aspinall
PGIP abstraction: PGML
--- a/src/Pure/ProofGeneral/proof_general_keywords.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_keywords.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/proof_general_keywords.ML
- ID: $Id$
Author: Makarius
Dummy session with outer syntax keyword initialization.
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/proof_general_pgip.ML
- ID: $Id$
Author: David Aspinall and Markus Wenzel
Isabelle configuration for Proof General using PGIP protocol.
--- a/src/Pure/Pure.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Pure.thy Wed Jan 21 23:42:37 2009 +0100
@@ -1,6 +1,3 @@
-(* Title: Pure/Pure.thy
- ID: $Id$
-*)
section {* Further content for the Pure theory *}
--- a/src/Pure/Thy/html.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Thy/html.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/html.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
HTML presentation elements.
--- a/src/Pure/Thy/latex.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Thy/latex.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/latex.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
LaTeX presentation elements -- based on outer lexical syntax.
--- a/src/Pure/Thy/present.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Thy/present.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/present.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Theory presentation: HTML, graph files, (PDF)LaTeX documents.
--- a/src/Pure/Thy/term_style.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Thy/term_style.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/term_style.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Styles for terms, to use with the "term_style" and "thm_style"
--- a/src/Pure/Thy/thm_deps.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thm_deps.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Visualize dependencies of theorems.
--- a/src/Pure/Thy/thy_header.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Thy/thy_header.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thy_header.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Theory headers -- independent of outer syntax.
--- a/src/Pure/Thy/thy_output.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thy_output.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Theory document output.
--- a/src/Pure/Tools/xml_syntax.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Tools/xml_syntax.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Tools/xml_syntax.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Input and output of types, terms, and proofs in XML format.
--- a/src/Pure/assumption.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/assumption.ML Wed Jan 21 23:42:37 2009 +0100
@@ -119,6 +119,6 @@
val thm = export false inner outer;
val term = export_term inner outer;
val typ = Logic.type_map term;
- in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = map thm} end;
+ in Morphism.morphism {binding = I, typ = typ, term = term, fact = map thm} end;
end;
--- a/src/Pure/config.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/config.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/config.ML
- ID: $Id$
Author: Makarius
Configuration options as values within the local context.
--- a/src/Pure/conjunction.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/conjunction.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/conjunction.ML
- ID: $Id$
Author: Makarius
Meta-level conjunction.
--- a/src/Pure/consts.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/consts.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/consts.ML
- ID: $Id$
Author: Makarius
Polymorphic constants: declarations, abbreviations, additional type
--- a/src/Pure/context_position.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/context_position.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/context_position.ML
- ID: $Id$
Author: Makarius
Context position visibility flag.
--- a/src/Pure/conv.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/conv.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/conv.ML
- ID: $Id$
Author: Amine Chaieb and Makarius
Conversions: primitive equality reasoning.
--- a/src/Pure/defs.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/defs.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/defs.ML
- ID: $Id$
Author: Makarius
Global well-formedness checks for constant definitions. Covers plain
--- a/src/Pure/display.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/display.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/display.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/Pure/interpretation.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/interpretation.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/interpretation.ML
- ID: $Id$
Author: Florian Haftmann and Makarius
Generic interpretation of theory data.
--- a/src/Pure/morphism.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/morphism.ML Wed Jan 21 23:42:37 2009 +0100
@@ -16,7 +16,6 @@
signature MORPHISM =
sig
include BASIC_MORPHISM
- val var: morphism -> binding * mixfix -> binding * mixfix
val binding: morphism -> binding -> binding
val typ: morphism -> typ -> typ
val term: morphism -> term -> term
@@ -25,12 +24,10 @@
val cterm: morphism -> cterm -> cterm
val morphism:
{binding: binding -> binding,
- var: binding * mixfix -> binding * mixfix,
typ: typ -> typ,
term: term -> term,
fact: thm list -> thm list} -> morphism
val binding_morphism: (binding -> binding) -> morphism
- val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism
val typ_morphism: (typ -> typ) -> morphism
val term_morphism: (term -> term) -> morphism
val fact_morphism: (thm list -> thm list) -> morphism
@@ -46,7 +43,6 @@
datatype morphism = Morphism of
{binding: binding -> binding,
- var: binding * mixfix -> binding * mixfix,
typ: typ -> typ,
term: term -> term,
fact: thm list -> thm list};
@@ -54,7 +50,6 @@
type declaration = morphism -> Context.generic -> Context.generic;
fun binding (Morphism {binding, ...}) = binding;
-fun var (Morphism {var, ...}) = var;
fun typ (Morphism {typ, ...}) = typ;
fun term (Morphism {term, ...}) = term;
fun fact (Morphism {fact, ...}) = fact;
@@ -63,20 +58,19 @@
val morphism = Morphism;
-fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I};
-fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I};
-fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I};
-fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I};
-fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact};
-fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm};
+fun binding_morphism binding = morphism {binding = binding, typ = I, term = I, fact = I};
+fun typ_morphism typ = morphism {binding = I, typ = typ, term = I, fact = I};
+fun term_morphism term = morphism {binding = I, typ = I, term = term, fact = I};
+fun fact_morphism fact = morphism {binding = I, typ = I, term = I, fact = fact};
+fun thm_morphism thm = morphism {binding = I, typ = I, term = I, fact = map thm};
-val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I};
+val identity = morphism {binding = I, typ = I, term = I, fact = I};
fun compose
- (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1})
- (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) =
- morphism {binding = binding1 o binding2, var = var1 o var2,
- typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
+ (Morphism {binding = binding1, typ = typ1, term = term1, fact = fact1})
+ (Morphism {binding = binding2, typ = typ2, term = term2, fact = fact2}) =
+ morphism {binding = binding1 o binding2, typ = typ1 o typ2,
+ term = term1 o term2, fact = fact1 o fact2};
fun phi1 $> phi2 = compose phi2 phi1;
--- a/src/Pure/net.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/net.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/net.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/Pure/old_goals.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/old_goals.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/old_goals.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/Pure/sign.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/sign.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/sign.ML
- ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
Logical signature content: naming conventions, concrete syntax, type
--- a/src/Pure/simplifier.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/simplifier.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/simplifier.ML
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
Generic simplifier, suitable for most logics (see also
--- a/src/Pure/subgoal.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/subgoal.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/subgoal.ML
- ID: $Id$
Author: Makarius
Tactical operations depending on local subgoal structure.
--- a/src/Pure/theory.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/theory.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/theory.ML
- ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
Logical theory content: axioms, definitions, and begin/end wrappers.
--- a/src/Pure/type_infer.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/type_infer.ML Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/type_infer.ML
- ID: $Id$
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
Simple type inference.
--- a/src/Pure/variable.ML Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/variable.ML Wed Jan 21 23:42:37 2009 +0100
@@ -397,7 +397,7 @@
val fact = export inner outer;
val term = singleton (export_terms inner outer);
val typ = Logic.type_map term;
- in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = fact} end;
+ in Morphism.morphism {binding = I, typ = typ, term = term, fact = fact} end;