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