changeset 48230 | 0feb93dfb268 |
parent 47991 | 3eb598b044ad |
child 48238 | c9454e434665 |
--- a/src/HOL/Tools/ATP/atp_util.ML Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Tue Jul 10 23:36:03 2012 +0200 @@ -192,6 +192,7 @@ | (k1, k2) => if k1 >= max orelse k2 >= max then max else Int.min (max, Integer.pow k2 k1)) + | Type (@{type_name set}, [T']) => aux slack avoid (T' --> @{typ bool}) | @{typ prop} => 2 | @{typ bool} => 2 (* optimization *) | @{typ nat} => 0 (* optimization *)