changeset 16417 | 9bc16273c2d4 |
parent 15032 | 02aed07e01bf |
child 17781 | 32bb237158a5 |
--- a/src/HOL/Hoare/HoareAbort.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Hoare/HoareAbort.thy Fri Jun 17 16:12:49 2005 +0200 @@ -6,8 +6,8 @@ Like Hoare.thy, but with an Abort statement for modelling run time errors. *) -theory HoareAbort = Main -files ("hoareAbort.ML"): +theory HoareAbort imports Main +uses ("hoareAbort.ML") begin types 'a bexp = "'a set"