# HG changeset patch
# User wenzelm
# Date 1608758722 -3600
# Node ID db8f94656024ebc496d839e6506acba8285339eb
# Parent  5906162c8dd45c14da9ebca01cd5c8266856f192
tuned document, notably authors and sections;

diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Arith2.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,12 +1,12 @@
 (*  Title:      HOL/Hoare/Arith2.thy
     Author:     Norbert Galm
     Copyright   1995 TUM
-
-More arithmetic.  Much of this duplicates ex/Primes.
 *)
 
+section \<open>More arithmetic\<close>
+
 theory Arith2
-imports Main
+  imports Main
 begin
 
 definition cd :: "[nat, nat, nat] \<Rightarrow> bool"
@@ -21,7 +21,7 @@
 | "fac (Suc n) = Suc n * fac n"
 
 
-subsubsection \<open>cd\<close>
+subsection \<open>cd\<close>
 
 lemma cd_nnn: "0<n \<Longrightarrow> cd n n n"
   apply (simp add: cd_def)
@@ -48,7 +48,7 @@
   done
 
 
-subsubsection \<open>gcd\<close>
+subsection \<open>gcd\<close>
 
 lemma gcd_nnn: "0<n \<Longrightarrow> n = gcd n n"
   apply (unfold gcd_def)
@@ -79,7 +79,7 @@
   done
 
 
-subsubsection \<open>pow\<close>
+subsection \<open>pow\<close>
 
 lemma sq_pow_div2 [simp]:
     "m mod 2 = 0 \<Longrightarrow> ((n::nat)*n)^(m div 2) = n^m"
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Examples.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -3,13 +3,15 @@
     Copyright   1998 TUM
 *)
 
-chapter \<open>Various examples\<close>
-
-theory Examples imports Hoare_Logic Arith2 begin
+section \<open>Various examples\<close>
 
-section \<open>ARITHMETIC\<close>
+theory Examples
+  imports Hoare_Logic Arith2
+begin
 
-subsection \<open>multiplication by successive addition\<close>
+subsection \<open>Arithmetic\<close>
+
+subsubsection \<open>Multiplication by successive addition\<close>
 
 lemma multiply_by_add: "VARS m s a b
   {a=A \<and> b=B}
@@ -54,7 +56,7 @@
 done
 
 
-subsection \<open>Euclid's algorithm for GCD\<close>
+subsubsection \<open>Euclid's algorithm for GCD\<close>
 
 lemma Euclid_GCD: "VARS a b
  {0<A & 0<B}
@@ -87,7 +89,7 @@
 done
 
 
-subsection \<open>Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\<close>
+subsubsection \<open>Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\<close>
 
 text \<open>
   From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
@@ -112,7 +114,7 @@
 done
 
 
-subsection \<open>Power by iterated squaring and multiplication\<close>
+subsubsection \<open>Power by iterated squaring and multiplication\<close>
 
 lemma power_by_mult: "VARS a b c
  {a=A & b=B}
@@ -132,7 +134,7 @@
 done
 
 
-subsection \<open>Factorial\<close>
+subsubsection \<open>Factorial\<close>
 
 lemma factorial: "VARS a b
  {a=A}
@@ -185,7 +187,7 @@
 done
 
 
-subsection \<open>Square root\<close>
+subsubsection \<open>Square root\<close>
 
 \<comment> \<open>the easy way:\<close>
 
@@ -221,7 +223,7 @@
 done
 
 
-section \<open>LISTS\<close>
+subsection \<open>Lists\<close>
 
 lemma imperative_reverse: "VARS y x
  {x=X}
@@ -276,9 +278,9 @@
 done
 
 
-section \<open>ARRAYS\<close>
+subsection \<open>Arrays\<close>
 
-subsection \<open>Search for a key\<close>
+subsubsection \<open>Search for a key\<close>
 
 lemma zero_search: "VARS A i
  {True}
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/ExamplesAbort.thy
--- a/src/HOL/Hoare/ExamplesAbort.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/ExamplesAbort.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,11 +1,13 @@
 (*  Title:      HOL/Hoare/ExamplesAbort.thy
     Author:     Tobias Nipkow
     Copyright   1998 TUM
-
-Some small examples for programs that may abort.
 *)
 
-theory ExamplesAbort imports Hoare_Logic_Abort begin
+section \<open>Some small examples for programs that may abort\<close>
+
+theory ExamplesAbort
+  imports Hoare_Logic_Abort
+begin
 
 lemma "VARS x y z::nat
  {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/ExamplesTC.thy
--- a/src/HOL/Hoare/ExamplesTC.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/ExamplesTC.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -5,9 +5,7 @@
 section \<open>Examples using Hoare Logic for Total Correctness\<close>
 
 theory ExamplesTC
-
-imports Hoare_Logic
-
+  imports Hoare_Logic
 begin
 
 text \<open>
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Heap.thy
--- a/src/HOL/Hoare/Heap.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Heap.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,12 +1,15 @@
 (*  Title:      HOL/Hoare/Heap.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
-
-Pointers, heaps and heap abstractions.
-See the paper by Mehta and Nipkow.
 *)
 
-theory Heap imports Main begin
+section \<open>Pointers, heaps and heap abstractions\<close>
+
+text \<open>See the paper by Mehta and Nipkow.\<close>
+
+theory Heap
+  imports Main
+begin
 
 subsection "References"
 
@@ -22,9 +25,9 @@
   "addr (Ref a) = a"
 
 
-section "The heap"
+subsection "The heap"
 
-subsection "Paths in the heap"
+subsubsection "Paths in the heap"
 
 primrec Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
   "Path h x [] y \<longleftrightarrow> x = y"
@@ -55,7 +58,7 @@
 by simp
 
 
-subsection "Non-repeating paths"
+subsubsection "Non-repeating paths"
 
 definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
   where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
@@ -78,9 +81,9 @@
 by (case_tac Ps, auto)
 
 
-subsection "Lists on the heap"
+subsubsection "Lists on the heap"
 
-subsubsection "Relational abstraction"
+paragraph "Relational abstraction"
 
 definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
   where "List h x as = Path h x as Null"
@@ -131,7 +134,7 @@
 done
 
 
-subsection "Functional abstraction"
+subsubsection "Functional abstraction"
 
 definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
   where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/HeapSyntax.thy
--- a/src/HOL/Hoare/HeapSyntax.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/HeapSyntax.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -3,7 +3,11 @@
     Copyright   2002 TUM
 *)
 
-theory HeapSyntax imports Hoare_Logic Heap begin
+section \<open>Heap syntax\<close>
+
+theory HeapSyntax
+  imports Hoare_Logic Heap
+begin
 
 subsection "Field access and update"
 
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/HeapSyntaxAbort.thy
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -3,7 +3,11 @@
     Copyright   2002 TUM
 *)
 
-theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin
+section \<open>Heap syntax (abort)\<close>
+
+theory HeapSyntaxAbort
+  imports Hoare_Logic_Abort Heap
+begin
 
 subsection "Field access and update"
 
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -4,7 +4,13 @@
     Author:     Walter Guttmann (extension to total-correctness proofs)
 *)
 
-section \<open>Sugared semantic embedding of Hoare logic\<close>
+section \<open>Hoare logic\<close>
+
+theory Hoare_Logic
+  imports Hoare_Syntax Hoare_Tac
+begin
+
+subsection \<open>Sugared semantic embedding of Hoare logic\<close>
 
 text \<open>
   Strictly speaking a shallow embedding (as implemented by Norbert Galm
@@ -12,10 +18,6 @@
   later.
 \<close>
 
-theory Hoare_Logic
-imports Hoare_Syntax Hoare_Tac
-begin
-
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 type_synonym 'a var = "'a \<Rightarrow> nat"
@@ -167,7 +169,7 @@
 qed
 
 
-subsection \<open>Concrete syntax\<close>
+subsubsection \<open>Concrete syntax\<close>
 
 setup \<open>
   Hoare_Syntax.setup
@@ -181,7 +183,7 @@
 \<close>
 
 
-subsection \<open>Proof methods: VCG\<close>
+subsubsection \<open>Proof methods: VCG\<close>
 
 declare BasicRule [Hoare_Tac.BasicRule]
   and SkipRule [Hoare_Tac.SkipRule]
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -7,7 +7,7 @@
 section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close>
 
 theory Hoare_Logic_Abort
-imports Hoare_Syntax Hoare_Tac
+  imports Hoare_Syntax Hoare_Tac
 begin
 
 type_synonym 'a bexp = "'a set"
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Hoare_Syntax.thy
--- a/src/HOL/Hoare/Hoare_Syntax.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Syntax.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Hoare/Hoare_Syntax.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Author:     Walter Guttmann (extension to total-correctness proofs)
+*)
 
-Concrete syntax for Hoare logic, with translations for variables.
-*)
+section \<open>Concrete syntax for Hoare logic, with translations for variables\<close>
 
 theory Hoare_Syntax
   imports Main
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Hoare_Tac.thy
--- a/src/HOL/Hoare/Hoare_Tac.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Tac.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Hoare/Hoare_Tac.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Author:     Walter Guttmann (extension to total-correctness proofs)
+*)
 
-Derivation of the proof rules and, most importantly, the VCG tactic.
-*)
+section \<open>Hoare logic VCG tactic\<close>
 
 theory Hoare_Tac
   imports Main
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,17 +1,20 @@
 (*  Title:      HOL/Hoare/Pointer_Examples.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
-
-Examples of verifications of pointer programs.
 *)
 
-theory Pointer_Examples imports HeapSyntax begin
+section \<open>Examples of verifications of pointer programs\<close>
+
+theory Pointer_Examples
+  imports HeapSyntax
+begin
 
 axiomatization where unproven: "PROP A"
 
-section "Verifications"
 
-subsection "List reversal"
+subsection "Verifications"
+
+subsubsection "List reversal"
 
 text "A short but unreadable proof:"
 
@@ -105,7 +108,7 @@
 done
 
 
-subsection "Searching in a list"
+subsubsection "Searching in a list"
 
 text\<open>What follows is a sequence of successively more intelligent proofs that
 a simple loop finds an element in a linked list.
@@ -174,7 +177,8 @@
 apply clarsimp
 done
 
-subsection "Splicing two lists"
+
+subsubsection "Splicing two lists"
 
 lemma "VARS tl p q pp qq
   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps}
@@ -204,7 +208,7 @@
 done
 
 
-subsection "Merging two lists"
+subsubsection "Merging two lists"
 
 text"This is still a bit rough, especially the proof."
 
@@ -392,7 +396,7 @@
 text"The proof is automatic, but requires a numbet of special lemmas."
 
 
-subsection "Cyclic list reversal"
+subsubsection "Cyclic list reversal"
 
 
 text\<open>We consider two algorithms for the reversal of circular lists.
@@ -468,7 +472,7 @@
 done
 
 
-subsection "Storage allocation"
+subsubsection "Storage allocation"
 
 definition new :: "'a set \<Rightarrow> 'a"
   where "new A = (SOME a. a \<notin> A)"
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Pointer_ExamplesAbort.thy
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,15 +1,17 @@
 (*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
-
-Examples of verifications of pointer programs
 *)
 
-theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
+section \<open>Examples of verifications of pointer programs\<close>
 
-section "Verifications"
+theory Pointer_ExamplesAbort
+  imports HeapSyntaxAbort
+begin
 
-subsection "List reversal"
+subsection "Verifications"
+
+subsubsection "List reversal"
 
 text "Interestingly, this proof is the same as for the unguarded program:"
 
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Pointers0.thy
--- a/src/HOL/Hoare/Pointers0.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Pointers0.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -9,7 +9,11 @@
 - in fact in some case they appear to get (a bit) more complicated.
 *)
 
-theory Pointers0 imports Hoare_Logic begin
+section \<open>Alternative pointers\<close>
+
+theory Pointers0
+  imports Hoare_Logic
+begin
 
 subsection "References"
 
@@ -40,9 +44,9 @@
 by vcg_simp
 
 
-section "The heap"
+subsection "The heap"
 
-subsection "Paths in the heap"
+subsubsection "Paths in the heap"
 
 primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
 where
@@ -68,9 +72,9 @@
 lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
 by(induct as, simp, simp add:eq_sym_conv)
 
-subsection "Lists on the heap"
+subsubsection "Lists on the heap"
 
-subsubsection "Relational abstraction"
+paragraph "Relational abstraction"
 
 definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
   where "List h x as = Path h x as Null"
@@ -118,7 +122,7 @@
 apply(fastforce dest:List_hd_not_in_tl)
 done
 
-subsection "Functional abstraction"
+subsubsection "Functional abstraction"
 
 definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
   where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
@@ -173,9 +177,9 @@
 done
 
 
-section "Verifications"
+subsection "Verifications"
 
-subsection "List reversal"
+subsubsection "List reversal"
 
 text "A short but unreadable proof:"
 
@@ -256,7 +260,7 @@
 done
 
 
-subsection "Searching in a list"
+subsubsection "Searching in a list"
 
 text\<open>What follows is a sequence of successively more intelligent proofs that
 a simple loop finds an element in a linked list.
@@ -312,7 +316,7 @@
 done
 
 
-subsection "Merging two lists"
+subsubsection "Merging two lists"
 
 text"This is still a bit rough, especially the proof."
 
@@ -398,7 +402,7 @@
 (* TODO: merging with islist/list instead of List: an improvement?
    needs (is)path, which is not so easy to prove either. *)
 
-subsection "Storage allocation"
+subsubsection "Storage allocation"
 
 definition new :: "'a set \<Rightarrow> 'a::ref"
   where "new A = (SOME a. a \<notin> A & a \<noteq> Null)"
@@ -427,5 +431,4 @@
  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
 done
 
-
 end
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/SchorrWaite.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,14 +1,15 @@
 (*  Title:      HOL/Hoare/SchorrWaite.thy
     Author:     Farhad Mehta
     Copyright   2003 TUM
-
-Proof of the Schorr-Waite graph marking algorithm.
 *)
 
+section \<open>Proof of the Schorr-Waite graph marking algorithm\<close>
 
-theory SchorrWaite imports HeapSyntax begin
+theory SchorrWaite
+  imports HeapSyntax
+begin
 
-section \<open>Machinery for the Schorr-Waite proof\<close>
+subsection \<open>Machinery for the Schorr-Waite proof\<close>
 
 definition
   \<comment> \<open>Relations induced by a mapping\<close>
@@ -194,8 +195,7 @@
 done
 
 
-section\<open>The Schorr-Waite algorithm\<close>
-
+subsection \<open>The Schorr-Waite algorithm\<close>
 
 theorem SchorrWaiteAlgorithm: 
 "VARS c m l r t p q root
@@ -573,4 +573,3 @@
   qed
 
 end
-
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/SepLogHeap.thy
--- a/src/HOL/Hoare/SepLogHeap.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,13 +1,14 @@
 (*  Title:      HOL/Hoare/SepLogHeap.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
-
-Heap abstractions (at the moment only Path and List)
-for Separation Logic.
 *)
 
+section \<open>Heap abstractions for Separation Logic\<close>
+
+text \<open>(at the moment only Path and List)\<close>
+
 theory SepLogHeap
-imports Main
+  imports Main
 begin
 
 type_synonym heap = "(nat \<Rightarrow> nat option)"
@@ -15,6 +16,7 @@
 text\<open>\<open>Some\<close> means allocated, \<open>None\<close> means
 free. Address \<open>0\<close> serves as the null reference.\<close>
 
+
 subsection "Paths in the heap"
 
 primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Separation.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -9,10 +9,13 @@
 into parser and pretty printer, which is not very modular.
 Alternative: some syntax like <P> which stands for P H. No more
 compact, but avoids the funny H.
-
 *)
 
-theory Separation imports Hoare_Logic_Abort SepLogHeap begin
+section \<open>Separation logic\<close>
+
+theory Separation
+  imports Hoare_Logic_Abort SepLogHeap
+begin
 
 text\<open>The semantic definition of a few connectives:\<close>
 
diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/document/root.tex
--- a/src/HOL/Hoare/document/root.tex	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/document/root.tex	Wed Dec 23 22:25:22 2020 +0100
@@ -1,4 +1,4 @@
-\documentclass[11pt,a4paper]{report}
+\documentclass[11pt,a4paper]{article}
 \usepackage{graphicx}
 \usepackage[english]{babel}
 \usepackage{isabelle,isabellesym}
@@ -10,7 +10,12 @@
 \begin{document}
 
 \title{Hoare Logic}
-\author{Various}
+\author{
+  Norbert Galm \\
+  Walter Guttmann \\
+  Farhad Mehta \\
+  Tobias Nipkow \\
+  Leonor Prensa Nieto}
 \maketitle
 
 \begin{abstract}
@@ -27,7 +32,11 @@
 \thispagestyle{empty}
 \tableofcontents
 
-\newpage
+\begin{center}
+  \includegraphics[scale=0.5]{session_graph}
+\end{center}
+
+\clearpage
 
 \input{session}