changeset 69605 | a96320074298 |
parent 66453 | cc19f7ca2ed6 |
child 76091 | 922e3f9251ac |
--- a/src/HOL/Prolog/HOHH.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Prolog/HOHH.thy Sun Jan 06 15:04:34 2019 +0100 @@ -8,7 +8,7 @@ imports HOL.HOL begin -ML_file "prolog.ML" +ML_file \<open>prolog.ML\<close> method_setup ptac = \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>