src/HOL/Import/hol4rews.ML
changeset 14620 1be590fd2422
parent 14518 c3019a66180f
child 14818 ad83019a66a4
     1.1 --- a/src/HOL/Import/hol4rews.ML	Sat Apr 17 20:04:23 2004 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Apr 17 23:53:35 2004 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  Title:      HOL/Import/hol4rews.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9  structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);
    1.10  
    1.11  type holthm = (term * term) list * thm
    1.12 @@ -24,7 +29,7 @@
    1.13  
    1.14  structure ImportSegmentArgs: THEORY_DATA_ARGS =
    1.15  struct
    1.16 -val name = "HOL4/import"
    1.17 +val name = "HOL4/import_segment"
    1.18  type T = string
    1.19  val empty = ""
    1.20  val copy = I