--- a/src/HOL/Bali/DefiniteAssignment.thy Wed May 14 15:22:37 2003 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Wed May 14 20:29:18 2003 +0200
@@ -511,7 +511,7 @@
nrm :: "lname set" --{* Definetly assigned variables
for normal completion*}
brk :: "breakass" --{* Definetly assigned variables for
- abnormal completion with a break *}
+ abrupt completion with a break *}
consts da :: "(env \<times> lname set \<times> term \<times> assigned) set"
text {* The environment @{term env} is only needed for the
@@ -638,7 +638,7 @@
and so we can't guarantee that any variable will be assigned in @{term c1}.
The @{text Finally} statement completes
normally if both @{term c1} and @{term c2} complete normally. If @{term c1}
- completes abnormally with a break, then @{term c2} also will be executed
+ completes abruptly with a break, then @{term c2} also will be executed
and may terminate normally or with a break. The overall break map then is
the intersection of the maps of both paths. If @{term c2} terminates
normally we have to extend all break sets in @{term "brk C1"} with