Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add header
authorhuffman
Wed, 20 Sep 2006 07:42:12 +0200
changeset 20634 45fe31e72391
parent 20633 e98f59806244
child 20635 e95db20977c5
add header
src/HOL/Real/Ferrante_Rackoff.thy file | annotate | diff | comparison | revisions
src/HOL/Real/RealPow.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Real/Ferrante_Rackoff.thy	Wed Sep 20 00:24:24 2006 +0200
+++ b/src/HOL/Real/Ferrante_Rackoff.thy	Wed Sep 20 07:42:12 2006 +0200
@@ -1,9 +1,9 @@
 (*
     ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
+*)
 
-Ferrante and Rackoff Algorithm: LCF-proof-synthesis version.
-*)
+header {* Ferrante and Rackoff Algorithm: LCF-proof-synthesis version. *}
 
 theory Ferrante_Rackoff
 imports RealPow
--- a/src/HOL/Real/RealPow.thy	Wed Sep 20 00:24:24 2006 +0200
+++ b/src/HOL/Real/RealPow.thy	Wed Sep 20 07:42:12 2006 +0200
@@ -2,9 +2,9 @@
     ID          : $Id$
     Author      : Jacques D. Fleuriot  
     Copyright   : 1998  University of Cambridge
-    Description : Natural powers theory
+*)
 
-*)
+header {* Natural powers theory *}
 
 theory RealPow
 imports RealDef
isabelle