equal
deleted
inserted
replaced
1160 (* FIXME: correspond to each other *) |
1160 (* FIXME: correspond to each other *) |
1161 in |
1161 in |
1162 #rel qinfo |
1162 #rel qinfo |
1163 end |
1163 end |
1164 | _ => HOLogic.eq_const dummyT |
1164 | _ => HOLogic.eq_const dummyT |
1165 (* FIXME: do the types correspond to each other? *) |
1165 (* FIXME: check that the types correspond to each other? *) |
1166 end |
1166 end |
1167 *} |
1167 *} |
1168 |
1168 |
1169 ML {* |
1169 ML {* |
1170 val mk_babs = Const (@{const_name "Babs"}, dummyT) |
1170 val mk_babs = Const (@{const_name "Babs"}, dummyT) |
1185 *} |
1185 *} |
1186 |
1186 |
1187 ML {* |
1187 ML {* |
1188 (* - applies f to the subterm of an abstraction, *) |
1188 (* - applies f to the subterm of an abstraction, *) |
1189 (* otherwise to the given term, *) |
1189 (* otherwise to the given term, *) |
1190 (* - used by REGUKARIZE, therefore abstracted *) |
1190 (* - used by REGULARIZE, therefore abstracted *) |
1191 (* variables do not have to be treated specially *) |
1191 (* variables do not have to be treated specially *) |
1192 |
1192 |
1193 fun apply_subt f trm1 trm2 = |
1193 fun apply_subt f trm1 trm2 = |
1194 case (trm1, trm2) of |
1194 case (trm1, trm2) of |
1195 (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') |
1195 (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') |
1255 in |
1255 in |
1256 if ty = ty' |
1256 if ty = ty' |
1257 then Const (@{const_name "Ex"}, ty) $ subtrm |
1257 then Const (@{const_name "Ex"}, ty) $ subtrm |
1258 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1258 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1259 end |
1259 end |
1260 (* FIXME: should be replaced when fully applied? then 2nd argument *) |
1260 (* FIXME: Should = only be replaced, when fully applied? *) |
|
1261 (* Then there must be a 2nd argument *) |
1261 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
1262 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
1262 let |
1263 let |
1263 val subtrm = REGULARIZE_trm lthy t t' |
1264 val subtrm = REGULARIZE_trm lthy t t' |
1264 in |
1265 in |
1265 if ty = ty' |
1266 if ty = ty' |