--- 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 ==>
--- a/src/HOL/NanoJava/Term.thy Mon Sep 10 18:18:04 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy Mon Sep 10 18:31:24 2001 +0200
@@ -31,8 +31,8 @@
| Comp stmt stmt ("_;; _" [91,90 ] 90)
| Cond expr stmt stmt ("If '(_') _ Else _" [99,91,91] 91)
| Loop vname stmt ("While '(_') _" [99,91 ] 91)
- | LAss vname expr ("_ :== _" [99, 95] 94) --{* local ass.*}
- | FAss expr fname expr ("_.._:==_" [95,99,95] 94) --{* field ass.*}
+ | LAss vname expr ("_ :== _" [99, 95] 94) --{* local assignment *}
+ | FAss expr fname expr ("_.._:==_" [95,99,95] 94) --{* field assignment *}
| Meth "cname \<times> mname" --{* virtual method *}
| Impl "cname \<times> mname" --{* method implementation *}
and expr
--- a/src/HOL/NanoJava/document/root.tex Mon Sep 10 18:18:04 2001 +0200
+++ b/src/HOL/NanoJava/document/root.tex Mon Sep 10 18:31:24 2001 +0200
@@ -9,11 +9,6 @@
\addtolength{\voffset}{-2cm}
\addtolength{\textheight}{4cm}
-%subsection instead of section to make the toc readable
-\renewcommand{\thesubsection}{\arabic{subsection}}
-\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
-\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
-
%remove spaces from the isabelle environment (trivlist makes them too large)
\renewenvironment{isabelle}
{\begin{isabellebody}}