equal
deleted
inserted
replaced
296 (* typ -> int *) |
296 (* typ -> int *) |
297 fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1) |
297 fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1) |
298 | card (Type ("*", [T1, T2])) = card T1 * card T2 |
298 | card (Type ("*", [T1, T2])) = card T1 * card T2 |
299 | card @{typ bool} = 2 |
299 | card @{typ bool} = 2 |
300 | card T = Int.max (1, raw_card T) |
300 | card T = Int.max (1, raw_card T) |
301 val neg_t = @{const Not} $ ObjectLogic.atomize_term thy t |
301 val neg_t = @{const Not} $ Object_Logic.atomize_term thy t |
302 val _ = fold_types (K o check_type ctxt) neg_t () |
302 val _ = fold_types (K o check_type ctxt) neg_t () |
303 val frees = Term.add_frees neg_t [] |
303 val frees = Term.add_frees neg_t [] |
304 val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees |
304 val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees |
305 val declarative_axioms = |
305 val declarative_axioms = |
306 map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees |
306 map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees |