src/HOL/BNF_Def.thy
changeset 72907 3883f536d84d
parent 69913 ca515cf61651
child 74886 fa5476c54731
equal deleted inserted replaced
72906:00399e5a6e50 72907:3883f536d84d