src/HOL/SMT_Examples/Boogie.thy
changeset 63167 0909deb8059b
parent 58889 5b7a9633cfa8
child 66740 ece9435ca78e
     1.1 --- a/src/HOL/SMT_Examples/Boogie.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/SMT_Examples/Boogie.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -2,14 +2,14 @@
     1.4      Author:     Sascha Boehme, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Proving Boogie-generated verification conditions *}
     1.8 +section \<open>Proving Boogie-generated verification conditions\<close>
     1.9  
    1.10  theory Boogie
    1.11  imports Main
    1.12  keywords "boogie_file" :: thy_load ("b2i")
    1.13  begin
    1.14  
    1.15 -text {*
    1.16 +text \<open>
    1.17  HOL-Boogie and its applications are described in:
    1.18  \begin{itemize}
    1.19  
    1.20 @@ -22,20 +22,20 @@
    1.21  Journal of Automated Reasoning, 2009.
    1.22  
    1.23  \end{itemize}
    1.24 -*}
    1.25 +\<close>
    1.26  
    1.27  
    1.28  
    1.29 -section {* Built-in types and functions of Boogie *}
    1.30 +section \<open>Built-in types and functions of Boogie\<close>
    1.31  
    1.32 -subsection {* Integer arithmetics *}
    1.33 +subsection \<open>Integer arithmetics\<close>
    1.34  
    1.35 -text {*
    1.36 -The operations @{text div} and @{text mod} are built-in in Boogie, but
    1.37 +text \<open>
    1.38 +The operations \<open>div\<close> and \<open>mod\<close> are built-in in Boogie, but
    1.39  without a particular semantics due to different interpretations in
    1.40  programming languages. We assume that each application comes with a
    1.41  proper axiomatization.
    1.42 -*}
    1.43 +\<close>
    1.44  
    1.45  axiomatization
    1.46    boogie_div :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div'_b" 70) and
    1.47 @@ -43,13 +43,13 @@
    1.48  
    1.49  
    1.50  
    1.51 -section {* Setup *}
    1.52 +section \<open>Setup\<close>
    1.53  
    1.54  ML_file "boogie.ML"
    1.55  
    1.56  
    1.57  
    1.58 -section {* Verification condition proofs *}
    1.59 +section \<open>Verification condition proofs\<close>
    1.60  
    1.61  declare [[smt_oracle = false]]
    1.62  declare [[smt_read_only_certificates = true]]