--- a/Admin/profiling_report Tue Aug 02 16:52:21 2005 +0200
+++ b/Admin/profiling_report Tue Aug 02 19:47:11 2005 +0200
@@ -27,7 +27,7 @@
}
foreach my $fun (keys %log) {
- push @output, (sprintf "%12d %s\n", $log{$fun}, $fun);
+ push @output, (sprintf "%14u %s\n", $log{$fun}, $fun);
}
print (sort @output);
--- a/etc/settings Tue Aug 02 16:52:21 2005 +0200
+++ b/etc/settings Tue Aug 02 19:47:11 2005 +0200
@@ -169,6 +169,9 @@
## Set HOME only for tools you have installed!
+# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
+HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
+
# SVC (Stanford Validity Checker)
#SVC_HOME=
#SVC_MACHINE=i386-redhat-linux
@@ -193,9 +196,6 @@
# Jerusat 1.3 (SAT Solver)
#JERUSAT_HOME=/usr/local/bin
-# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
-HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
-
# For configuring HOL/Matrix/cplex
# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
# First option: use the commercial cplex solver
--- a/src/ZF/pair.thy Tue Aug 02 16:52:21 2005 +0200
+++ b/src/ZF/pair.thy Tue Aug 02 19:47:11 2005 +0200
@@ -129,7 +129,8 @@
lemma expand_split:
"u: A*B ==>
R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
-apply (simp add: split_def, auto)
+apply (simp add: split_def)
+apply auto
done