src/HOL/Tools/recdef.ML
changeset 47470 335a1bd76710
parent 47067 4ef29b0c568f
child 47815 43f677b3ae91
equal deleted inserted replaced
47469:ba7fe841c885 47470:335a1bd76710