# HG changeset patch
# User oheimb
# Date 995907971 -7200
# Node ID d25be0ad1a6ca8db8450585e3f3a3bb09139de1e
# Parent  aa519e0cc050d2270933eea60aec6b5c5922678f
cosmetics

diff -r aa519e0cc050 -r d25be0ad1a6c src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Mon Jul 23 17:47:49 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Mon Jul 23 19:06:11 2001 +0200
@@ -100,9 +100,9 @@
 by (auto intro: hoare.ConjI hoare.ConjE)
 
 lemma Impl': 
- "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
+  "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
                 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
-      A     ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
+       A    ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
 apply (drule Union[THEN iffD2])
 apply (drule hoare.Impl)
 apply (drule Union[THEN iffD1])
@@ -110,10 +110,10 @@
 done
 
 lemma Impl1: 
- "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
+   "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
                  (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms; 
-  (C,m)\<in> ms\<rbrakk> \<Longrightarrow> 
-       A    \<turnstile> {P z C m} Impl C m {Q (z::state) C m}"
+    (C,m)\<in> ms\<rbrakk> \<Longrightarrow> 
+         A             |- {P z C m} Impl C m {Q (z::state) C m}"
 apply (drule Impl')
 apply (erule Weaken)
 apply (auto del: image_eqI intro: rev_image_eqI)