doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
changeset 28564 1358b1ddd915
parent 28561 056255ade52a
child 28593 f087237af65d
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 10 06:49:44 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 10 15:23:33 2008 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4    SML code:
     1.5  *}
     1.6  
     1.7 -primrec %quoteme in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
     1.8 +primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
     1.9    "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
    1.10  (*<*)
    1.11  code_type %invisible bool
    1.12 @@ -124,7 +124,7 @@
    1.13  code_const %invisible True and False and "op \<and>" and Not
    1.14    (SML and and and)
    1.15  (*>*)
    1.16 -text %quoteme {*@{code_stmts in_interval (SML)}*}
    1.17 +text %quote {*@{code_stmts in_interval (SML)}*}
    1.18  
    1.19  text {*
    1.20    \noindent Though this is correct code, it is a little bit unsatisfactory:
    1.21 @@ -138,9 +138,9 @@
    1.22    \qn{custom serialisations}:
    1.23  *}
    1.24  
    1.25 -code_type %tt bool
    1.26 +code_type %quotett bool
    1.27    (SML "bool")
    1.28 -code_const %tt True and False and "op \<and>"
    1.29 +code_const %quotett True and False and "op \<and>"
    1.30    (SML "true" and "false" and "_ andalso _")
    1.31  
    1.32  text {*
    1.33 @@ -155,7 +155,7 @@
    1.34    for the type constructor's (the constant's) arguments.
    1.35  *}
    1.36  
    1.37 -text %quoteme {*@{code_stmts in_interval (SML)}*}
    1.38 +text %quote {*@{code_stmts in_interval (SML)}*}
    1.39  
    1.40  text {*
    1.41    \noindent This still is not perfect: the parentheses
    1.42 @@ -166,10 +166,10 @@
    1.43    associative infixes with precedences which may be used here:
    1.44  *}
    1.45  
    1.46 -code_const %tt "op \<and>"
    1.47 +code_const %quotett "op \<and>"
    1.48    (SML infixl 1 "andalso")
    1.49  
    1.50 -text %quoteme {*@{code_stmts in_interval (SML)}*}
    1.51 +text %quote {*@{code_stmts in_interval (SML)}*}
    1.52  
    1.53  text {*
    1.54    \noindent The attentive reader may ask how we assert that no generated
    1.55 @@ -180,7 +180,7 @@
    1.56    accidental overwrites, using the @{command "code_reserved"} command:
    1.57  *}
    1.58  
    1.59 -code_reserved %quoteme "SML " bool true false andalso
    1.60 +code_reserved %quote "SML " bool true false andalso
    1.61  
    1.62  text {*
    1.63    \noindent Next, we try to map HOL pairs to SML pairs, using the
    1.64 @@ -192,9 +192,9 @@
    1.65  code_const %invisible Pair
    1.66    (SML)
    1.67  (*>*)
    1.68 -code_type %tt *
    1.69 +code_type %quotett *
    1.70    (SML infix 2 "*")
    1.71 -code_const %tt Pair
    1.72 +code_const %quotett Pair
    1.73    (SML "!((_),/ (_))")
    1.74  
    1.75  text {*
    1.76 @@ -232,10 +232,10 @@
    1.77    @{const HOL.eq}
    1.78  *}
    1.79  
    1.80 -code_class %tt eq
    1.81 +code_class %quotett eq
    1.82    (Haskell "Eq" where "HOL.eq" \<equiv> "(==)")
    1.83  
    1.84 -code_const %tt "op ="
    1.85 +code_const %quotett "op ="
    1.86    (Haskell infixl 4 "==")
    1.87  
    1.88  text {*
    1.89 @@ -245,18 +245,18 @@
    1.90    of @{text Haskell} @{text Eq}:
    1.91  *}
    1.92  
    1.93 -typedecl %quoteme bar
    1.94 +typedecl %quote bar
    1.95  
    1.96 -instantiation %quoteme bar :: eq
    1.97 +instantiation %quote bar :: eq
    1.98  begin
    1.99  
   1.100 -definition %quoteme "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
   1.101 +definition %quote "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
   1.102  
   1.103 -instance %quoteme by default (simp add: eq_bar_def)
   1.104 +instance %quote by default (simp add: eq_bar_def)
   1.105  
   1.106 -end %quoteme
   1.107 +end %quote
   1.108  
   1.109 -code_type %tt bar
   1.110 +code_type %quotett bar
   1.111    (Haskell "Integer")
   1.112  
   1.113  text {*
   1.114 @@ -267,7 +267,7 @@
   1.115    @{text "code_instance"}:
   1.116  *}
   1.117  
   1.118 -code_instance %tt bar :: eq
   1.119 +code_instance %quotett bar :: eq
   1.120    (Haskell -)
   1.121  
   1.122  
   1.123 @@ -279,10 +279,10 @@
   1.124    command:
   1.125  *}
   1.126  
   1.127 -code_include %tt Haskell "Errno"
   1.128 +code_include %quotett Haskell "Errno"
   1.129  {*errno i = error ("Error number: " ++ show i)*}
   1.130  
   1.131 -code_reserved %tt Haskell Errno
   1.132 +code_reserved %quotett Haskell Errno
   1.133  
   1.134  text {*
   1.135    \noindent Such named @{text include}s are then prepended to every generated code.