src/HOL/UNITY/FP.thy
changeset 13798 4c1a53627500
parent 13796 19f50fa807ae
child 13812 91713a1915ee
--- a/src/HOL/UNITY/FP.thy	Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/FP.thy	Fri Jan 31 20:12:44 2003 +0100
@@ -3,11 +3,11 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Fixed Point of a Program
-
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
+header{*Fixed Point of a Program*}
+
 theory FP = UNITY:
 
 constdefs