equal
deleted
inserted
replaced
46 kind = Thm.internalK, |
46 kind = Thm.internalK, |
47 alt_name = Binding.empty, |
47 alt_name = Binding.empty, |
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 skip_mono = true, |
|
52 fork_mono = false} |
52 [((Binding.name R, T), NoSyn)] (* the relation *) |
53 [((Binding.name R, T), NoSyn)] (* the relation *) |
53 [] (* no parameters *) |
54 [] (* no parameters *) |
54 (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *) |
55 (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *) |
55 [] (* no special monos *) |
56 [] (* no special monos *) |
56 lthy |
57 lthy |