equal
deleted
inserted
replaced
71 fun close p t f = |
71 fun close p t f = |
72 let val vs = Term.add_vars t [] |
72 let val vs = Term.add_vars t [] |
73 in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs)) |
73 in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs)) |
74 (p (fold (Logic.all o Var) vs t) f) |
74 (p (fold (Logic.all o Var) vs t) f) |
75 end; |
75 end; |
76 fun mkop "op &" T x = SOME (Const (@{const_name "Int"}, T --> T --> T), x) |
76 fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x) |
77 | mkop "op |" T x = SOME (Const (@{const_name "Un"}, T --> T --> T), x) |
77 | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x) |
78 | mkop _ _ _ = NONE; |
78 | mkop _ _ _ = NONE; |
79 fun mk_collect p T t = |
79 fun mk_collect p T t = |
80 let val U = HOLogic.dest_setT T |
80 let val U = HOLogic.dest_setT T |
81 in HOLogic.Collect_const U $ |
81 in HOLogic.Collect_const U $ |
82 HOLogic.ap_split' (HOLogic.prod_factors p) U HOLogic.boolT t |
82 HOLogic.ap_split' (HOLogic.prod_factors p) U HOLogic.boolT t |