# HG changeset patch
# User wenzelm
# Date 1123004831 -7200
# Node ID 51ff2bc327741d337f0b30f9229d7391bd1af25d
# Parent  552df70f52c221c3a86e74c80e3cb9b2bbf9d1b8
tuned;

diff -r 552df70f52c2 -r 51ff2bc32774 Admin/profiling_report
--- 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);
diff -r 552df70f52c2 -r 51ff2bc32774 etc/settings
--- 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
diff -r 552df70f52c2 -r 51ff2bc32774 src/ZF/pair.thy
--- 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