Lines Matching defs:ax
24 {ax : shared_thm,
350 val {ax,case_def,case_eq,case_cong,induction,
376 axiom = ax,
393 local fun mk_ti (n,ax,ind)
395 mk_datatype_info{ax=COPY(n,ax), induction=COPY(n,ind),
402 :: mk_ti (n,ax,ind) cds cgs oos ds nchs
407 fun gen_datatype_info {ax, ind, case_defs} =
410 val one_ones = prove_constructors_one_one ax
411 val distincts = prove_constructors_distinct ax
421 {ax=ORIG ax, induction=ORIG ind,
432 in tyinfo_1 :: mk_ti (tyname,ax,ind)