equal
deleted
inserted
replaced
1010 else |
1010 else |
1011 card_of_type assigns T |
1011 card_of_type assigns T |
1012 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => |
1012 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => |
1013 default_card) |
1013 default_card) |
1014 |
1014 |
1015 (* Similar to "ATP_Translate.tiny_card_of_type". *) |
1015 (* Similar to "ATP_Util.tiny_card_of_type". *) |
1016 fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card |
1016 fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card |
1017 assigns T = |
1017 assigns T = |
1018 let |
1018 let |
1019 fun aux avoid T = |
1019 fun aux avoid T = |
1020 (if member (op =) avoid T then |
1020 (if member (op =) avoid T then |