equal
deleted
inserted
replaced
138 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
138 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
139 |
139 |
140 |
140 |
141 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm |
141 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm |
142 |
142 |
143 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
143 fun mk_all (a, T) t = Logic.all_const T $ Abs (a, T, t) |
144 |
144 |
145 fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) |
145 fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) |
146 |
146 |
147 fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) |
147 fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) |
148 |
148 |