src/HOL/Recdef.thy
changeset 41615 f70d2cb26acf
parent 39302 d7728f65b353
equal deleted inserted replaced
41614:b7cd80330a16 41615:f70d2cb26acf