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 ***)