src/HOL/Extraction.thy
changeset 60758 d8d85a8172b5
parent 60169 5ef8ed685965
child 62922 96691631c1eb
     1.1 --- a/src/HOL/Extraction.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Stefan Berghofer, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Program extraction for HOL *}
     1.8 +section \<open>Program extraction for HOL\<close>
     1.9  
    1.10  theory Extraction
    1.11  imports Option
    1.12 @@ -10,9 +10,9 @@
    1.13  
    1.14  ML_file "Tools/rewrite_hol_proof.ML"
    1.15  
    1.16 -subsection {* Setup *}
    1.17 +subsection \<open>Setup\<close>
    1.18  
    1.19 -setup {*
    1.20 +setup \<open>
    1.21    Extraction.add_types
    1.22        [("bool", ([], NONE))] #>
    1.23    Extraction.set_preprocessor (fn thy =>
    1.24 @@ -22,7 +22,7 @@
    1.25          (RewriteHOLProof.rews,
    1.26           ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
    1.27        ProofRewriteRules.elim_vars (curry Const @{const_name default}))
    1.28 -*}
    1.29 +\<close>
    1.30  
    1.31  lemmas [extraction_expand] =
    1.32    meta_spec atomize_eq atomize_all atomize_imp atomize_conj
    1.33 @@ -40,7 +40,7 @@
    1.34  
    1.35  datatype (plugins only: code extraction) sumbool = Left | Right
    1.36  
    1.37 -subsection {* Type of extracted program *}
    1.38 +subsection \<open>Type of extracted program\<close>
    1.39  
    1.40  extract_type
    1.41    "typeof (Trueprop P) \<equiv> typeof P"
    1.42 @@ -90,7 +90,7 @@
    1.43  
    1.44    "typeof (x \<in> P) \<equiv> typeof P"
    1.45  
    1.46 -subsection {* Realizability *}
    1.47 +subsection \<open>Realizability\<close>
    1.48  
    1.49  realizability
    1.50    "(realizes t (Trueprop P)) \<equiv> (Trueprop (realizes t P))"
    1.51 @@ -150,7 +150,7 @@
    1.52  
    1.53    "(realizes t (P = Q)) \<equiv> (realizes t ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)))"
    1.54  
    1.55 -subsection {* Computational content of basic inference rules *}
    1.56 +subsection \<open>Computational content of basic inference rules\<close>
    1.57  
    1.58  theorem disjE_realizer:
    1.59    assumes r: "case x of Inl p \<Rightarrow> P p | Inr q \<Rightarrow> Q q"