1.1 --- a/test/Tools/isac/Knowledge/Isac.thy	Sun Oct 10 14:15:43 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/Isac.thy	Mon Oct 11 12:55:40 2010 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:  test/Tools/isac/Isac.thy
     1.5 -    Author: Walther Neuper, TU Graz
     1.6 +    Author: Walther Neuper, TU Graz, 2010
     1.7 +    (c) due to copyright terms
     1.8  
     1.9  12345678901234567890123456789012345678901234567890123456789012345678901234567890
    1.10          10        20        30        40        50        60        70        80
    1.11 @@ -7,7 +8,8 @@
    1.12  
    1.13  theory Isac imports Complex_Main (*TODO Build_Isac*) begin
    1.14  
    1.15 -section {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals *}
    1.16 +text {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals;
    1.17 +        the leading parts of longnames can be dropped with some exceptions. *}
    1.18  
    1.19  lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)"          by (rule List.take_Cons)
    1.20  lemma "t = (t::real)"                                                           by (rule HOL.refl)