# HG changeset patch
# User oheimb
# Date 1000139484 -7200
# Node ID 46d0bde121abe4d6a40bf35f2585b21e1a1239e2
# Parent  65d98faa2182f9999e70764ac392c2fb0c36b619
marginally improved comments

diff -r 65d98faa2182 -r 46d0bde121ab src/HOL/NanoJava/AxSem.thy
--- 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 ==>
diff -r 65d98faa2182 -r 46d0bde121ab src/HOL/NanoJava/Term.thy
--- 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
diff -r 65d98faa2182 -r 46d0bde121ab src/HOL/NanoJava/document/root.tex
--- 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}}