equal
deleted
inserted
replaced
600 verbose = ! trace, |
600 verbose = ! trace, |
601 alt_name = Binding.empty, |
601 alt_name = Binding.empty, |
602 coind = false, |
602 coind = false, |
603 no_elim = false, |
603 no_elim = false, |
604 no_ind = false, |
604 no_ind = false, |
605 skip_mono = true, |
605 skip_mono = true} |
606 fork_mono = false} |
|
607 [binding] (* relation *) |
606 [binding] (* relation *) |
608 [] (* no parameters *) |
607 [] (* no parameters *) |
609 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) |
608 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) |
610 [] (* no special monos *) |
609 [] (* no special monos *) |
611 ||> Local_Theory.restore_naming lthy |
610 ||> Local_Theory.restore_naming lthy |