| changeset 58825 | 2065f49da190 |
| parent 58184 | db1381d811ab |
| child 58881 | b9556a055632 |
--- a/src/HOL/Library/Old_Recdef.thy Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Library/Old_Recdef.thy Wed Oct 29 17:01:44 2014 +0100 @@ -68,7 +68,7 @@ ML_file "~~/src/HOL/Tools/TFL/tfl.ML" ML_file "~~/src/HOL/Tools/TFL/post.ML" ML_file "~~/src/HOL/Tools/recdef.ML" -setup Recdef.setup + subsection {* Rule setup *}