--- a/src/HOL/NanoJava/AxSem.thy Mon Sep 10 18:18:04 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Mon Sep 10 18:31:24 2001 +0200
@@ -4,7 +4,7 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-header "Axiomatic Semantics (Hoare Logic)"
+header "Axiomatic Semantics"
theory AxSem = State:
@@ -42,6 +42,8 @@
"A \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)"
+subsection "Hoare Logic Rules"
+
inductive hoare ehoare
intros
@@ -86,7 +88,7 @@
Impl (D,m) {Q} ==>
A |- {P} Meth (C,m) {Q}"
- --{* @{text "\<Union>z"} instead of @{text "\<forall>z"} in the conclusion and
+ --{* @{text "\<Union>z"} instead of @{text "\<forall>z"} in the conclusion and\\
z restricted to type state due to limitations of the inductive package *}
Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||-
(\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==>