tuned;
authorwenzelm
Thu, 26 Jul 2012 13:35:31 +0200
changeset 49527a69d7dc49f41
parent 49526 37999ee01156
child 49528 ace120a2cb70
tuned;
src/HOL/ROOT
src/Pure/System/build.ML
     1.1 --- a/src/HOL/ROOT	Thu Jul 26 12:59:09 2012 +0200
     1.2 +++ b/src/HOL/ROOT	Thu Jul 26 13:35:31 2012 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    options [document = false]
     1.5    theories Main
     1.6  
     1.7 -session "HOL-Proofs"! (main) in "." = Pure +
     1.8 +session "HOL-Proofs"! in "." = Pure +
     1.9    description {* HOL-Main with explicit proof terms *}
    1.10    options [document = false, proofs = 2, parallel_proofs = 0]
    1.11    theories Main
     2.1 --- a/src/Pure/System/build.ML	Thu Jul 26 12:59:09 2012 +0200
     2.2 +++ b/src/Pure/System/build.ML	Thu Jul 26 13:35:31 2012 +0200
     2.3 @@ -42,7 +42,7 @@
     2.4      (case filter_out (can getenv_strict) condition of
     2.5        [] => use_thys options thys
     2.6      | conds =>
     2.7 -        Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
     2.8 +        Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
     2.9            " (undefined " ^ commas conds ^ ")\n"))
    2.10    end;
    2.11