src/HOL/Library/Old_Recdef.thy
changeset 58825 2065f49da190
parent 58184 db1381d811ab
child 58881 b9556a055632
equal deleted inserted replaced
58824:d480d1d7c544 58825:2065f49da190
    66 ML_file "~~/src/HOL/Tools/TFL/rules.ML"
    66 ML_file "~~/src/HOL/Tools/TFL/rules.ML"
    67 ML_file "~~/src/HOL/Tools/TFL/thry.ML"
    67 ML_file "~~/src/HOL/Tools/TFL/thry.ML"
    68 ML_file "~~/src/HOL/Tools/TFL/tfl.ML"
    68 ML_file "~~/src/HOL/Tools/TFL/tfl.ML"
    69 ML_file "~~/src/HOL/Tools/TFL/post.ML"
    69 ML_file "~~/src/HOL/Tools/TFL/post.ML"
    70 ML_file "~~/src/HOL/Tools/recdef.ML"
    70 ML_file "~~/src/HOL/Tools/recdef.ML"
    71 setup Recdef.setup
    71 
    72 
    72 
    73 subsection {* Rule setup *}
    73 subsection {* Rule setup *}
    74 
    74 
    75 lemmas [recdef_simp] =
    75 lemmas [recdef_simp] =
    76   inv_image_def
    76   inv_image_def