src/HOL/Hoare/Examples.thy
changeset 35316 870dfea4f9c0
parent 16796 140f1e0ea846
child 42154 478bdcea240a
     1.1 --- a/src/HOL/Hoare/Examples.thy	Tue Feb 23 10:11:12 2010 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Tue Feb 23 10:11:15 2010 +0100
     1.3 @@ -1,12 +1,11 @@
     1.4  (*  Title:      HOL/Hoare/Examples.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Norbert Galm
     1.7      Copyright   1998 TUM
     1.8  
     1.9  Various examples.
    1.10  *)
    1.11  
    1.12 -theory Examples imports Hoare Arith2 begin
    1.13 +theory Examples imports Hoare_Logic Arith2 begin
    1.14  
    1.15  (*** ARITHMETIC ***)
    1.16