--- 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
--- 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
--- 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 *)
--- 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 ##;
--- 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;
--- 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
--- 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.
*)
--- 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 =