src/HOL/Induct/Common_Patterns.thy
changeset 28741 1b257449f804
parent 24609 3f238d4987c0
child 29961 c7849326100e
equal deleted inserted replaced
28740:22a8125d66fa 28741:1b257449f804