equal
deleted
inserted
replaced
429 by (rule partial_term_of_anything) |
429 by (rule partial_term_of_anything) |
430 |
430 |
431 *) |
431 *) |
432 |
432 |
433 hide_type code_int narrowing_type narrowing_term cons property |
433 hide_type code_int narrowing_type narrowing_term cons property |
434 hide_const int_of of_int nth error toEnum marker empty |
434 hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists |
435 C cons conv nonEmpty "apply" sum ensure_testable all exists |
435 hide_const (open) Var Ctr "apply" sum cons |
436 hide_const (open) Var Ctr |
|
437 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def |
436 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def |
438 |
437 |
439 |
438 |
440 end |
439 end |