tuned;
authorwenzelm
Mon, 01 Oct 2001 15:46:35 +0200
changeset 11649 dfb59b9954a6
parent 11648 d78a82d112e4
child 11650 e4314c06a2a3
tuned;
src/HOL/Induct/ABexp.thy
src/HOL/Induct/Ordinals.thy
src/HOL/Induct/Term.thy
src/HOL/Induct/Tree.thy
--- 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 *}