changeset 30738 | 0842e906300c |
parent 27487 | c8a6ce181805 |
child 37757 | dc78d2d9e90a |
--- a/src/HOL/Library/While_Combinator.thy Fri Mar 27 10:05:08 2009 +0100 +++ b/src/HOL/Library/While_Combinator.thy Fri Mar 27 10:05:11 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Library/While_Combinator.thy - ID: $Id$ Author: Tobias Nipkow Copyright 2000 TU Muenchen *) @@ -7,7 +6,7 @@ header {* A general ``while'' combinator *} theory While_Combinator -imports Plain "~~/src/HOL/Presburger" +imports Main begin text {*