Lines Matching defs:defs
33 fun num_values REP_ABS defs =
34 let val len = length defs
43 map rep_of defs
248 val defs = map (new_definition o def) nclist
249 val constrs = map (lhs o concl) defs
253 defs = defs,
356 val abs_thm = save_thm (abs_name, LIST_CONJ (map SYM (#defs result)))
359 LIST_CONJ (num_values (#REP_ABS result) (#defs result)))
363 val nchotomy = prove_cases_thm (#ABS_ONTO result) (List.rev (#defs result))
420 val {TYPE,constrs,defs, ABSconst, REPconst,
429 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
432 val {TYPE,constrs,defs, ABSconst, REPconst,
444 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
447 val {TYPE,constrs,defs, ABSconst, REPconst,
459 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
463 val {TYPE,constrs,defs, ABSconst, REPconst,
477 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
480 val {TYPE,constrs,defs, ABSconst, REPconst,
495 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
498 val {TYPE,constrs,defs, ABSconst, REPconst,
516 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);
520 val {TYPE,constrs,defs, ABSconst, REPconst,
541 val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs);