src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 43368 0dc67b3cf8a5
parent 41075 4bed56dc95fb
child 44241 7943b69f0188
equal deleted inserted replaced
43367:3f1469de9e47 43368:0dc67b3cf8a5