1.1 --- a/src/HOL/Induct/ABexp.thy	Mon Oct 01 14:47:02 2001 +0200
     1.2 +++ b/src/HOL/Induct/ABexp.thy	Mon Oct 01 15:46:35 2001 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Induct/ABexp.thy
     1.5      ID:         $Id$
     1.6      Author:     Stefan Berghofer, TU Muenchen
     1.7 -    Copyright   1998  TU Muenchen
     1.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  *)
    1.10  
    1.11  header {* Arithmetic and boolean expressions *}

     2.1 --- a/src/HOL/Induct/Ordinals.thy	Mon Oct 01 14:47:02 2001 +0200
     2.2 +++ b/src/HOL/Induct/Ordinals.thy	Mon Oct 01 15:46:35 2001 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Induct/Tree.thy
     2.5 +(*  Title:      HOL/Induct/Ordinals.thy
     2.6      ID:         $Id$
     2.7      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     2.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.9 @@ -10,7 +10,7 @@
    2.10  
    2.11  text {*
    2.12    Some basic definitions of ordinal numbers.  Draws an Agda
    2.13 -  development (in Martin-L{\"}of type theory) by Peter Hancock (see
    2.14 +  development (in Martin-L\"of type theory) by Peter Hancock (see
    2.15    \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
    2.16  *}
    2.17  
    2.18 @@ -68,8 +68,8 @@
    2.19    "veb a == veblen a Zero"
    2.20  
    2.21  constdefs
    2.22 -  epsilon0 :: ordinal    ("SOME \<^sub>0")
    2.23 -  "SOME \<^sub>0 == veb Zero"
    2.24 +  epsilon0 :: ordinal    ("\<epsilon>\<^sub>0")
    2.25 +  "\<epsilon>\<^sub>0 == veb Zero"
    2.26    Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
    2.27    "\<Gamma>\<^sub>0 == Limit (\<lambda>n. iter veb n Zero)"
    2.28  

     3.1 --- a/src/HOL/Induct/Term.thy	Mon Oct 01 14:47:02 2001 +0200
     3.2 +++ b/src/HOL/Induct/Term.thy	Mon Oct 01 15:46:35 2001 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      HOL/Induct/Term.thy
     3.5      ID:         $Id$
     3.6      Author:     Stefan Berghofer,  TU Muenchen
     3.7 -    Copyright   1998  TU Muenchen
     3.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.9  *)
    3.10  
    3.11  header {* Terms over a given alphabet *}

     4.1 --- a/src/HOL/Induct/Tree.thy	Mon Oct 01 14:47:02 2001 +0200
     4.2 +++ b/src/HOL/Induct/Tree.thy	Mon Oct 01 15:46:35 2001 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      HOL/Induct/Tree.thy
     4.5      ID:         $Id$
     4.6      Author:     Stefan Berghofer,  TU Muenchen
     4.7 -    Copyright   1999  TU Muenchen
     4.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.9  *)
    4.10  
    4.11  header {* Infinitely branching trees *}