src/HOL/Induct/Exp.ML
changeset 5191 8ceaa19f7717
parent 5148 74919e8f221c
child 5223 4cb05273f764
equal deleted inserted replaced
5190:4ae031622592 5191:8ceaa19f7717