equal
deleted
inserted
replaced
41 let |
41 let |
42 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = |
42 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = |
43 InductivePackage.add_inductive_i |
43 InductivePackage.add_inductive_i |
44 {verbose = ! Toplevel.debug, |
44 {verbose = ! Toplevel.debug, |
45 kind = Thm.internalK, |
45 kind = Thm.internalK, |
|
46 group = serial_string (), (* FIXME pass proper group (!?) *) |
46 alt_name = "", |
47 alt_name = "", |
47 coind = false, |
48 coind = false, |
48 no_elim = false, |
49 no_elim = false, |
49 no_ind = false} |
50 no_ind = false} |
50 [((R, T), NoSyn)] (* the relation *) |
51 [((R, T), NoSyn)] (* the relation *) |