src/HOL/Library/Code_Test.thy
changeset 69593 3dda49e08b9d
parent 68484 59793df7f853
child 69605 a96320074298
     1.1 --- a/src/HOL/Library/Code_Test.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Library/Code_Test.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  keywords "test_code" :: diag
     1.5  begin
     1.6  
     1.7 -subsection \<open>YXML encoding for @{typ Code_Evaluation.term}\<close>
     1.8 +subsection \<open>YXML encoding for \<^typ>\<open>Code_Evaluation.term\<close>\<close>
     1.9  
    1.10  datatype (plugins del: code size "quickcheck") yxml_of_term = YXML
    1.11  
    1.12 @@ -24,7 +24,7 @@
    1.13  definition yot_concat :: "yxml_of_term list \<Rightarrow> yxml_of_term"
    1.14    where [code del]: "yot_concat _ = YXML"
    1.15  
    1.16 -text \<open>Serialise @{typ yxml_of_term} to native string of target language\<close>
    1.17 +text \<open>Serialise \<^typ>\<open>yxml_of_term\<close> to native string of target language\<close>
    1.18  
    1.19  code_printing type_constructor yxml_of_term
    1.20    \<rightharpoonup>  (SML) "string"
    1.21 @@ -55,7 +55,7 @@
    1.22  text \<open>
    1.23    Stripped-down implementations of Isabelle's XML tree with YXML encoding as
    1.24    defined in \<^file>\<open>~~/src/Pure/PIDE/xml.ML\<close>, \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close>
    1.25 -  sufficient to encode @{typ "Code_Evaluation.term"} as in
    1.26 +  sufficient to encode \<^typ>\<open>Code_Evaluation.term\<close> as in
    1.27    \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
    1.28  \<close>
    1.29  
    1.30 @@ -114,7 +114,7 @@
    1.31  where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
    1.32  
    1.33  text \<open>
    1.34 -  Encoding @{typ Code_Evaluation.term} into XML trees as defined in
    1.35 +  Encoding \<^typ>\<open>Code_Evaluation.term\<close> into XML trees as defined in
    1.36    \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
    1.37  \<close>
    1.38  
    1.39 @@ -132,8 +132,8 @@
    1.40    "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
    1.41    "xml_of_term (Code_Evaluation.App t1 t2)  = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]"
    1.42    "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]"
    1.43 -  \<comment> \<open>FIXME: @{const Code_Evaluation.Free} is used only in @{theory "HOL.Quickcheck_Narrowing"} to represent
    1.44 -    uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.\<close>
    1.45 +  \<comment> \<open>FIXME: \<^const>\<open>Code_Evaluation.Free\<close> is used only in \<^theory>\<open>HOL.Quickcheck_Narrowing\<close> to represent
    1.46 +    uninstantiated parameters in constructors. Here, we always translate them to \<^ML>\<open>Free\<close> variables.\<close>
    1.47    "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
    1.48  by(simp_all add: xml_of_term_def xml_tree_anything)
    1.49