equal
deleted
inserted
replaced
1530 |
1530 |
1531 fun register_bnf_raw key bnf = |
1531 fun register_bnf_raw key bnf = |
1532 Local_Theory.declaration {syntax = false, pervasive = true} |
1532 Local_Theory.declaration {syntax = false, pervasive = true} |
1533 (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))); |
1533 (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))); |
1534 |
1534 |
1535 fun register_bnf key bnf = register_bnf_raw key bnf #> interpret_bnf bnf; |
1535 fun register_bnf key bnf = |
|
1536 register_bnf_raw key bnf #> interpret_bnf bnf; |
1536 |
1537 |
1537 fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs = |
1538 fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs = |
1538 (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) => |
1539 (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) => |
1539 let |
1540 let |
1540 fun mk_wits_tac ctxt set_maps = |
1541 fun mk_wits_tac ctxt set_maps = |