equal
deleted
inserted
replaced
2293 (* setup theory *) |
2293 (* setup theory *) |
2294 |
2294 |
2295 val setup = |
2295 val setup = |
2296 Sign.add_trfuns ([], parse_translation, [], []) #> |
2296 Sign.add_trfuns ([], parse_translation, [], []) #> |
2297 Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #> |
2297 Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #> |
2298 (fn thy => (Simplifier.change_simpset_of thy |
2298 Simplifier.map_simpset (fn ss => |
2299 (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy)); |
2299 ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); |
2300 |
2300 |
2301 (* outer syntax *) |
2301 (* outer syntax *) |
2302 |
2302 |
2303 local structure P = OuterParse and K = OuterKeyword in |
2303 local structure P = OuterParse and K = OuterKeyword in |
2304 |
2304 |