equal
deleted
inserted
replaced
45 verbose = ! Toplevel.debug, |
45 verbose = ! Toplevel.debug, |
46 kind = Thm.internalK, |
46 kind = Thm.internalK, |
47 alt_name = "", |
47 alt_name = "", |
48 coind = false, |
48 coind = false, |
49 no_elim = false, |
49 no_elim = false, |
50 no_ind = false} |
50 no_ind = false, |
|
51 skip_mono = true} |
51 [((R, T), NoSyn)] (* the relation *) |
52 [((R, T), NoSyn)] (* the relation *) |
52 [] (* no parameters *) |
53 [] (* no parameters *) |
53 (map (fn t => (("", []), t)) defs) (* the intros *) |
54 (map (fn t => (("", []), t)) defs) (* the intros *) |
54 [] (* no special monos *) |
55 [] (* no special monos *) |
55 lthy |
56 lthy |