src/HOL/NSA/HTranscendental.thy
changeset 58878 f962e42e324d
parent 58656 7f14d5d9b933
child 59658 0cc388370041
equal deleted inserted replaced
58877:262572d90bc6 58878:f962e42e324d
     3     Copyright   : 2001 University of Edinburgh
     3     Copyright   : 2001 University of Edinburgh
     4 
     4 
     5 Converted to Isar and polished by lcp
     5 Converted to Isar and polished by lcp
     6 *)
     6 *)
     7 
     7 
     8 header{*Nonstandard Extensions of Transcendental Functions*}
     8 section{*Nonstandard Extensions of Transcendental Functions*}
     9 
     9 
    10 theory HTranscendental
    10 theory HTranscendental
    11 imports Transcendental HSeries HDeriv
    11 imports Transcendental HSeries HDeriv
    12 begin
    12 begin
    13 
    13