changeset 69605 | a96320074298 |
parent 69597 | ff784d5a5bfb |
child 70749 | 5d06b7bb9d22 |
--- a/src/HOL/Transitive_Closure.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Transitive_Closure.thy Sun Jan 06 15:04:34 2019 +0100 @@ -12,7 +12,7 @@ and "^=" = "\<^sup>=" "\<^sup>=\<^sup>=" begin -ML_file "~~/src/Provers/trancl.ML" +ML_file \<open>~~/src/Provers/trancl.ML\<close> text \<open> \<open>rtrancl\<close> is reflexive/transitive closure,