Lines Matching defs:failwith
168 fun failwith function =
171 fun fail () = failwith "fail";
201 else failwith "CHECK_TAC";
206 else failwith "FALSE_TAC";
217 else failwith "UNASSUME_TAC";
234 handle _ => failwith "FORALL_EQ_TAC";
245 handle _ => failwith "EXISTS_EQ_TAC";
256 fun find_exists_eq [] = failwith "find_exists_eq"
262 else failwith "find_exists_eq"
268 handle _ => failwith "FIND_EXISTS_TAC";
283 handle _ => failwith "UNBETA_TAC";
300 handle _ => failwith "WELL_FOUNDED_NUM_TAC";
319 handle _ => failwith "FORALL_IMP";
335 handle _ => failwith "FORALL_IMP_TAC";
355 handle _ => failwith "DEFINE_NEW_VAR";
388 handle _ => failwith "FORALL_SYM_CONV";
401 handle _ => failwith "NOT_AP_TERM_TAC";
413 handle _ => failwith "APP_LET_CONV";
428 handle _ => failwith "STRIP_let_TAC";
436 handle _ => failwith "USE_IMP_EQ_matches";
443 handle _ => failwith "USE_IMP_matches";
455 else (failwith "SUB_matches");
473 handle _ => failwith "USE_IMP_THEN";
488 handle _ => failwith "USE_THEN";