src/HOL/Predicate.thy
changeset 41265 a393d6d8e198
parent 41082 9ff94e7cc3b3
child 41311 de0c906dfe60