| changeset 67443 | 3abf6a722518 |
| parent 63680 | 6e1e8b5abbfa |
| child 67613 | ce654b0e6d69 |
--- a/src/HOL/Isar_Examples/Hoare.thy Tue Jan 16 09:12:16 2018 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Tue Jan 16 09:30:00 2018 +0100 @@ -400,7 +400,7 @@ lemma Compl_Collect: "- Collect b = {x. \<not> b x}" by blast -lemmas AbortRule = SkipRule \<comment> "dummy version" +lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close> ML_file "~~/src/HOL/Hoare/hoare_tac.ML"