tuned;
authorwenzelm
Wed Sep 06 16:54:12 2000 +0200 (2000-09-06)
changeset 9876a069795f1060
parent 9875 c50349d252b7
child 9877 b2a62260f8ac
tuned;
Admin/makedist
TFL/dcterm.sml
TFL/rules.sml
TFL/usyntax.sml
TFL/utils.sml
src/HOL/Main.thy
src/HOL/Tools/recdef_package.ML
src/HOL/simpdata.ML
     1.1 --- a/Admin/makedist	Wed Sep 06 13:32:25 2000 +0200
     1.2 +++ b/Admin/makedist	Wed Sep 06 16:54:12 2000 +0200
     1.3 @@ -110,7 +110,8 @@
     1.4  cd "$DISTBASE"
     1.5  
     1.6  $EXPORT
     1.7 -find . -name CVS -exec rm -rf {} \;
     1.8 +find . -name CVS -print | xargs rm -rf
     1.9 +find . -type d -a -empty -print | xargs rm -rf
    1.10  
    1.11  
    1.12  # build docs
     2.1 --- a/TFL/dcterm.sml	Wed Sep 06 13:32:25 2000 +0200
     2.2 +++ b/TFL/dcterm.sml	Wed Sep 06 16:54:12 2000 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      TFL/dcterm
     2.5 +(*  Title:      TFL/dcterm.sml
     2.6      ID:         $Id$
     2.7      Author:     Konrad Slind, Cambridge University Computer Laboratory
     2.8      Copyright   1997  University of Cambridge
     3.1 --- a/TFL/rules.sml	Wed Sep 06 13:32:25 2000 +0200
     3.2 +++ b/TFL/rules.sml	Wed Sep 06 16:54:12 2000 +0200
     3.3 @@ -8,7 +8,6 @@
     3.4  
     3.5  signature Rules_sig =
     3.6  sig
     3.7 -(*  structure USyntax : USyntax_sig *)
     3.8    val dest_thm : thm -> term list * term
     3.9  
    3.10    (* Inference rules *)
     4.1 --- a/TFL/usyntax.sml	Wed Sep 06 13:32:25 2000 +0200
     4.2 +++ b/TFL/usyntax.sml	Wed Sep 06 16:54:12 2000 +0200
     4.3 @@ -8,8 +8,6 @@
     4.4  
     4.5  signature USyntax_sig =
     4.6  sig
     4.7 -  structure Utils : Utils_sig
     4.8 -
     4.9    datatype lambda = VAR   of {Name : string, Ty : typ}
    4.10                    | CONST of {Name : string, Ty : typ}
    4.11                    | COMB  of {Rator: term, Rand : term}
    4.12 @@ -98,7 +96,6 @@
    4.13  structure USyntax : USyntax_sig =
    4.14  struct
    4.15  
    4.16 -structure Utils = Utils;
    4.17  open Utils;
    4.18  
    4.19  infix 4 ##;
     5.1 --- a/TFL/utils.sml	Wed Sep 06 13:32:25 2000 +0200
     5.2 +++ b/TFL/utils.sml	Wed Sep 06 16:54:12 2000 +0200
     5.3 @@ -102,5 +102,4 @@
     5.4  end;
     5.5  
     5.6  
     5.7 -
     5.8 -end; (* Utils *)
     5.9 +end;
     6.1 --- a/src/HOL/Main.thy	Wed Sep 06 13:32:25 2000 +0200
     6.2 +++ b/src/HOL/Main.thy	Wed Sep 06 16:54:12 2000 +0200
     6.3 @@ -6,6 +6,6 @@
     6.4  
     6.5  (*actually belongs to theory List*)
     6.6  lemmas [mono] = lists_mono
     6.7 -lemmas [recdef_cong] = map_cong 
     6.8 +lemmas [recdef_cong] = map_cong
     6.9  
    6.10  end
     7.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Sep 06 13:32:25 2000 +0200
     7.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Sep 06 16:54:12 2000 +0200
     7.3 @@ -1,6 +1,7 @@
     7.4  (*  Title:      HOL/Tools/recdef_package.ML
     7.5      ID:         $Id$
     7.6      Author:     Markus Wenzel, TU Muenchen
     7.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.8  
     7.9  Wrapper module for Konrad Slind's TFL package.
    7.10  *)
     8.1 --- a/src/HOL/simpdata.ML	Wed Sep 06 13:32:25 2000 +0200
     8.2 +++ b/src/HOL/simpdata.ML	Wed Sep 06 16:54:12 2000 +0200
     8.3 @@ -496,7 +496,7 @@
     8.4     ref_tac: int -> tactic
     8.5     the actual refutation tactic. Should be able to deal with goals
     8.6     [| A1; ...; An |] ==> False
     8.7 -   where the Ai are atomic, i.e. no top-level &, | or ?
     8.8 +   where the Ai are atomic, i.e. no top-level &, | or EX
     8.9  *)
    8.10  
    8.11  fun refute_tac test prep_tac ref_tac =