equal
deleted
inserted
replaced
28 |
28 |
29 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
29 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
30 fun mk_all_imp (A,P) = |
30 fun mk_all_imp (A,P) = |
31 FOLogic.all_const iT $ |
31 FOLogic.all_const iT $ |
32 Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ |
32 Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ |
33 betapply(P, Bound 0)); |
33 Term.betapply(P, Bound 0)); |
34 |
34 |
35 val Part_const = Const("Part", [iT,iT-->iT]--->iT); |
35 val Part_const = Const("Part", [iT,iT-->iT]--->iT); |
36 |
36 |
37 val apply_const = Const("op `", [iT,iT]--->iT); |
37 val apply_const = Const("op `", [iT,iT]--->iT); |
38 |
38 |