src/HOL/Import/HOL/seq.imp
changeset 17694 b7870c2bd7df
parent 14516 a183dec876ab
child 44763 b50d5d694838
     1.1 --- a/src/HOL/Import/HOL/seq.imp	Wed Sep 28 11:50:15 2005 +0200
     1.2 +++ b/src/HOL/Import/HOL/seq.imp	Wed Sep 28 13:17:23 2005 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4    "subseq" > "subseq_def"
     1.5    "mono" > "mono_def"
     1.6    "lim" > "lim_def"
     1.7 +  "hol4-->" > "hol4-->_def"
     1.8    "convergent" > "convergent_def"
     1.9    "cauchy" > "cauchy_def"
    1.10 -  "-->" > "-->_def"
    1.11  
    1.12  const_maps
    1.13    "sums" > "HOL4Real.seq.sums"
    1.14 @@ -20,9 +20,12 @@
    1.15    "subseq" > "HOL4Real.seq.subseq"
    1.16    "mono" > "HOL4Real.seq.mono"
    1.17    "lim" > "HOL4Real.seq.lim"
    1.18 +  "hol4-->" > "HOL4Real.seq.hol4-->"
    1.19    "convergent" > "HOL4Real.seq.convergent"
    1.20    "cauchy" > "HOL4Real.seq.cauchy"
    1.21 -  "-->" > "HOL4Real.seq.-->"
    1.22 +
    1.23 +const_renames
    1.24 +  "-->" > "hol4-->"
    1.25  
    1.26  thm_maps
    1.27    "tends_num_real" > "HOL4Real.seq.tends_num_real"
    1.28 @@ -38,6 +41,7 @@
    1.29    "mono" > "HOL4Real.seq.mono"
    1.30    "lim_def" > "HOL4Real.seq.lim_def"
    1.31    "lim" > "HOL4Real.seq.lim"
    1.32 +  "hol4-->_def" > "HOL4Real.seq.hol4-->_def"
    1.33    "convergent_def" > "HOL4Real.seq.convergent_def"
    1.34    "convergent" > "HOL4Real.seq.convergent"
    1.35    "cauchy_def" > "HOL4Real.seq.cauchy_def"
    1.36 @@ -104,6 +108,5 @@
    1.37    "GP" > "HOL4Real.seq.GP"
    1.38    "BOLZANO_LEMMA" > "HOL4Real.seq.BOLZANO_LEMMA"
    1.39    "ABS_NEG_LEMMA" > "HOL4Real.seq.ABS_NEG_LEMMA"
    1.40 -  "-->_def" > "HOL4Real.seq.-->_def"
    1.41  
    1.42  end