tuned;
authorwenzelm
Tue Aug 02 19:47:11 2005 +0200 (2005-08-02)
changeset 1700151ff2bc32774
parent 17000 552df70f52c2
child 17002 fb9261990ffe
tuned;
Admin/profiling_report
etc/settings
src/ZF/pair.thy
     1.1 --- a/Admin/profiling_report	Tue Aug 02 16:52:21 2005 +0200
     1.2 +++ b/Admin/profiling_report	Tue Aug 02 19:47:11 2005 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  }
     1.5  
     1.6  foreach my $fun (keys %log) {
     1.7 -    push @output, (sprintf "%12d %s\n", $log{$fun}, $fun);
     1.8 +    push @output, (sprintf "%14u %s\n", $log{$fun}, $fun);
     1.9  }
    1.10  
    1.11  print (sort @output);
     2.1 --- a/etc/settings	Tue Aug 02 16:52:21 2005 +0200
     2.2 +++ b/etc/settings	Tue Aug 02 19:47:11 2005 +0200
     2.3 @@ -169,6 +169,9 @@
     2.4  
     2.5  ## Set HOME only for tools you have installed!
     2.6  
     2.7 +# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
     2.8 +HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
     2.9 +
    2.10  # SVC (Stanford Validity Checker)
    2.11  #SVC_HOME=
    2.12  #SVC_MACHINE=i386-redhat-linux
    2.13 @@ -193,9 +196,6 @@
    2.14  # Jerusat 1.3 (SAT Solver)
    2.15  #JERUSAT_HOME=/usr/local/bin
    2.16  
    2.17 -# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
    2.18 -HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
    2.19 -
    2.20  # For configuring HOL/Matrix/cplex
    2.21  # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
    2.22  # First option: use the commercial cplex solver
     3.1 --- a/src/ZF/pair.thy	Tue Aug 02 16:52:21 2005 +0200
     3.2 +++ b/src/ZF/pair.thy	Tue Aug 02 19:47:11 2005 +0200
     3.3 @@ -129,7 +129,8 @@
     3.4  lemma expand_split: 
     3.5    "u: A*B ==>    
     3.6          R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
     3.7 -apply (simp add: split_def, auto)
     3.8 +apply (simp add: split_def)
     3.9 +apply auto
    3.10  done
    3.11  
    3.12