src/HOL/Hoare/Examples.thy
changeset 35316 870dfea4f9c0
parent 16796 140f1e0ea846
child 42154 478bdcea240a
--- a/src/HOL/Hoare/Examples.thy	Tue Feb 23 10:11:12 2010 +0100
+++ b/src/HOL/Hoare/Examples.thy	Tue Feb 23 10:11:15 2010 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Hoare/Examples.thy
-    ID:         $Id$
     Author:     Norbert Galm
     Copyright   1998 TUM
 
 Various examples.
 *)
 
-theory Examples imports Hoare Arith2 begin
+theory Examples imports Hoare_Logic Arith2 begin
 
 (*** ARITHMETIC ***)