src/HOL/Library/Reflection.thy
changeset 60500 903bb1495239
parent 59582 0fbed69ff081
child 61476 1884c40f1539
     1.1 --- a/src/HOL/Library/Reflection.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Reflection.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Amine Chaieb, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Generic reflection and reification *}
     1.8 +section \<open>Generic reflection and reification\<close>
     1.9  
    1.10  theory Reflection
    1.11  imports Main
    1.12 @@ -10,13 +10,13 @@
    1.13  
    1.14  ML_file "~~/src/HOL/Tools/reflection.ML"
    1.15  
    1.16 -method_setup reify = {*
    1.17 +method_setup reify = \<open>
    1.18    Attrib.thms --
    1.19      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
    1.20        (fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to))
    1.21 -*} "partial automatic reification"
    1.22 +\<close> "partial automatic reification"
    1.23  
    1.24 -method_setup reflection = {*
    1.25 +method_setup reflection = \<open>
    1.26  let
    1.27    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    1.28    val onlyN = "only";
    1.29 @@ -30,7 +30,7 @@
    1.30    (fn ((user_eqs, user_thms), to) => fn ctxt =>
    1.31          SIMPLE_METHOD' (Reflection.default_reflection_tac ctxt user_thms user_eqs to))
    1.32  end
    1.33 -*} "partial automatic reflection"
    1.34 +\<close> "partial automatic reflection"
    1.35  
    1.36  end
    1.37