Lines Matching defs:defs
32 fun num_values REP_ABS defs =
33 let val len = length defs
42 map rep_of defs
247 val defs = map (new_definition o def) nclist
248 val constrs = map (lhs o concl) defs
252 defs = defs,
355 val abs_thm = save_thm (abs_name, LIST_CONJ (map SYM (#defs result)))
358 LIST_CONJ (num_values (#REP_ABS result) (#defs result)))
362 val nchotomy = prove_cases_thm (#ABS_ONTO result) (List.rev (#defs result))
419 val {TYPE,constrs,defs, ABSconst, REPconst,
428 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
431 val {TYPE,constrs,defs, ABSconst, REPconst,
443 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
446 val {TYPE,constrs,defs, ABSconst, REPconst,
458 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
462 val {TYPE,constrs,defs, ABSconst, REPconst,
476 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
479 val {TYPE,constrs,defs, ABSconst, REPconst,
494 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
497 val {TYPE,constrs,defs, ABSconst, REPconst,
515 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
519 val {TYPE,constrs,defs, ABSconst, REPconst,
540 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);