equal
deleted
inserted
replaced
76 if member (op =) names name then SOME (f p q) else NONE |
76 if member (op =) names name then SOME (f p q) else NONE |
77 | _ => NONE) |
77 | _ => NONE) |
78 | split_conj _ _ _ _ = NONE; |
78 | split_conj _ _ _ _ = NONE; |
79 |
79 |
80 fun strip_all [] t = t |
80 fun strip_all [] t = t |
81 | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t; |
81 | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t; |
82 |
82 |
83 (*********************************************************************) |
83 (*********************************************************************) |
84 (* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *) |
84 (* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *) |
85 (* or ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t) *) |
85 (* or ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t) *) |
86 (* to R ... & id (ALL z. P z (pi_1 o ... o pi_n o t)) *) |
86 (* to R ... & id (ALL z. P z (pi_1 o ... o pi_n o t)) *) |