# HG changeset patch
# User wenzelm
# Date 968252052 -7200
# Node ID a069795f106017e6a74cda248d465acfdadfa8a6
# Parent  c50349d252b7749ef5c079ef9112dd9e6f839595
tuned;

diff -r c50349d252b7 -r a069795f1060 Admin/makedist
--- a/Admin/makedist	Wed Sep 06 13:32:25 2000 +0200
+++ b/Admin/makedist	Wed Sep 06 16:54:12 2000 +0200
@@ -110,7 +110,8 @@
 cd "$DISTBASE"
 
 $EXPORT
-find . -name CVS -exec rm -rf {} \;
+find . -name CVS -print | xargs rm -rf
+find . -type d -a -empty -print | xargs rm -rf
 
 
 # build docs
diff -r c50349d252b7 -r a069795f1060 TFL/dcterm.sml
--- a/TFL/dcterm.sml	Wed Sep 06 13:32:25 2000 +0200
+++ b/TFL/dcterm.sml	Wed Sep 06 16:54:12 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      TFL/dcterm
+(*  Title:      TFL/dcterm.sml
     ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
diff -r c50349d252b7 -r a069795f1060 TFL/rules.sml
--- a/TFL/rules.sml	Wed Sep 06 13:32:25 2000 +0200
+++ b/TFL/rules.sml	Wed Sep 06 16:54:12 2000 +0200
@@ -8,7 +8,6 @@
 
 signature Rules_sig =
 sig
-(*  structure USyntax : USyntax_sig *)
   val dest_thm : thm -> term list * term
 
   (* Inference rules *)
diff -r c50349d252b7 -r a069795f1060 TFL/usyntax.sml
--- a/TFL/usyntax.sml	Wed Sep 06 13:32:25 2000 +0200
+++ b/TFL/usyntax.sml	Wed Sep 06 16:54:12 2000 +0200
@@ -8,8 +8,6 @@
 
 signature USyntax_sig =
 sig
-  structure Utils : Utils_sig
-
   datatype lambda = VAR   of {Name : string, Ty : typ}
                   | CONST of {Name : string, Ty : typ}
                   | COMB  of {Rator: term, Rand : term}
@@ -98,7 +96,6 @@
 structure USyntax : USyntax_sig =
 struct
 
-structure Utils = Utils;
 open Utils;
 
 infix 4 ##;
diff -r c50349d252b7 -r a069795f1060 TFL/utils.sml
--- a/TFL/utils.sml	Wed Sep 06 13:32:25 2000 +0200
+++ b/TFL/utils.sml	Wed Sep 06 16:54:12 2000 +0200
@@ -102,5 +102,4 @@
 end;
 
 
-
-end; (* Utils *)
+end;
diff -r c50349d252b7 -r a069795f1060 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Sep 06 13:32:25 2000 +0200
+++ b/src/HOL/Main.thy	Wed Sep 06 16:54:12 2000 +0200
@@ -6,6 +6,6 @@
 
 (*actually belongs to theory List*)
 lemmas [mono] = lists_mono
-lemmas [recdef_cong] = map_cong 
+lemmas [recdef_cong] = map_cong
 
 end
diff -r c50349d252b7 -r a069795f1060 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Sep 06 13:32:25 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Wed Sep 06 16:54:12 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Tools/recdef_package.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Wrapper module for Konrad Slind's TFL package.
 *)
diff -r c50349d252b7 -r a069795f1060 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Sep 06 13:32:25 2000 +0200
+++ b/src/HOL/simpdata.ML	Wed Sep 06 16:54:12 2000 +0200
@@ -496,7 +496,7 @@
    ref_tac: int -> tactic
    the actual refutation tactic. Should be able to deal with goals
    [| A1; ...; An |] ==> False
-   where the Ai are atomic, i.e. no top-level &, | or ?
+   where the Ai are atomic, i.e. no top-level &, | or EX
 *)
 
 fun refute_tac test prep_tac ref_tac =