isabelle: src/HOL/Tools/recdef.ML@105bbce656a5 (annotated)

31723 f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 31243 diff changeset	1	(* Title: HOL/Tools/recdef.ML
6429 9771ce553e56 Wrapper module for Konrad Slind's TFL package. wenzelm parents: diff changeset	2	Author: Markus Wenzel, TU Muenchen
9771ce553e56 Wrapper module for Konrad Slind's TFL package. wenzelm parents: diff changeset	3
9771ce553e56 Wrapper module for Konrad Slind's TFL package. wenzelm parents: diff changeset	4	Wrapper module for Konrad Slind's TFL package.
9771ce553e56 Wrapper module for Konrad Slind's TFL package. wenzelm parents: diff changeset	5	*)
9771ce553e56 Wrapper module for Konrad Slind's TFL package. wenzelm parents: diff changeset	6