equal
deleted
inserted
replaced
446 by (rule partial_term_of_anything) |
446 by (rule partial_term_of_anything) |
447 |
447 |
448 *) |
448 *) |
449 |
449 |
450 hide_type code_int narrowing_type narrowing_term cons property |
450 hide_type code_int narrowing_type narrowing_term cons property |
451 hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists |
451 hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero |
452 hide_const (open) Var Ctr "apply" sum cons |
452 hide_const (open) Var Ctr "apply" sum cons |
453 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def |
453 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def |
454 |
454 |
455 |
455 |
456 end |
456 end |