tuned comments;
authorwenzelm
Wed, 24 Oct 2007 19:21:38 +0200
changeset 25172ad25033f9ca4
parent 25171 4a9c25bffc9b
child 25173 7e1f197a36c5
tuned comments;
lib/Tools/mkdir
src/HOL/hologic.ML
     1.1 --- a/lib/Tools/mkdir	Wed Oct 24 18:36:09 2007 +0200
     1.2 +++ b/lib/Tools/mkdir	Wed Oct 24 19:21:38 2007 +0200
     1.3 @@ -251,6 +251,7 @@
     1.4  
     1.5  \tableofcontents
     1.6  
     1.7 +% sane default for proof documents
     1.8  %\parindent 0pt\parskip 0.5ex
     1.9  
    1.10  % generated text of all theories
     2.1 --- a/src/HOL/hologic.ML	Wed Oct 24 18:36:09 2007 +0200
     2.2 +++ b/src/HOL/hologic.ML	Wed Oct 24 19:21:38 2007 +0200
     2.3 @@ -329,12 +329,11 @@
     2.4    in ap [T] end;
     2.5  
     2.6  
     2.7 -(***********************************************************)
     2.8 -(*       operations on tuples with specific arities        *)
     2.9 -(*                                                         *)
    2.10 -(* an "arity" of a tuple is a list of lists of integers    *)
    2.11 -(* ("factors"), denoting paths to subterms that are pairs  *)
    2.12 -(***********************************************************)
    2.13 +(* operations on tuples with specific arities *)
    2.14 +(*
    2.15 +  an "arity" of a tuple is a list of lists of integers
    2.16 +  ("factors"), denoting paths to subterms that are pairs
    2.17 +*)
    2.18  
    2.19  fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
    2.20