--- a/src/HOL/Induct/ABexp.thy Mon Oct 01 14:47:02 2001 +0200
+++ b/src/HOL/Induct/ABexp.thy Mon Oct 01 15:46:35 2001 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Induct/ABexp.thy
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1998 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Arithmetic and boolean expressions *}
--- a/src/HOL/Induct/Ordinals.thy Mon Oct 01 14:47:02 2001 +0200
+++ b/src/HOL/Induct/Ordinals.thy Mon Oct 01 15:46:35 2001 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Induct/Tree.thy
+(* Title: HOL/Induct/Ordinals.thy
ID: $Id$
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -10,7 +10,7 @@
text {*
Some basic definitions of ordinal numbers. Draws an Agda
- development (in Martin-L{\"}of type theory) by Peter Hancock (see
+ development (in Martin-L\"of type theory) by Peter Hancock (see
\url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
*}
@@ -68,8 +68,8 @@
"veb a == veblen a Zero"
constdefs
- epsilon0 :: ordinal ("SOME \<^sub>0")
- "SOME \<^sub>0 == veb Zero"
+ epsilon0 :: ordinal ("\<epsilon>\<^sub>0")
+ "\<epsilon>\<^sub>0 == veb Zero"
Gamma0 :: ordinal ("\<Gamma>\<^sub>0")
"\<Gamma>\<^sub>0 == Limit (\<lambda>n. iter veb n Zero)"
--- a/src/HOL/Induct/Term.thy Mon Oct 01 14:47:02 2001 +0200
+++ b/src/HOL/Induct/Term.thy Mon Oct 01 15:46:35 2001 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Induct/Term.thy
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1998 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Terms over a given alphabet *}
--- a/src/HOL/Induct/Tree.thy Mon Oct 01 14:47:02 2001 +0200
+++ b/src/HOL/Induct/Tree.thy Mon Oct 01 15:46:35 2001 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Induct/Tree.thy
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1999 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Infinitely branching trees *}