equal
deleted
inserted
replaced
606 |
606 |
607 local |
607 local |
608 |
608 |
609 fun add_decl loc decl = |
609 fun add_decl loc decl = |
610 add_thmss loc "" |
610 add_thmss loc "" |
611 [((Binding.concealed Binding.empty, |
611 [((Binding.empty, [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]), |
612 [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]), |
|
613 [([Drule.dummy_thm], [])])]; |
612 [([Drule.dummy_thm], [])])]; |
614 |
613 |
615 in |
614 in |
616 |
615 |
617 fun add_declaration loc syntax decl = |
616 fun add_declaration loc syntax decl = |