equal
deleted
inserted
replaced
476 Scan.succeed asm_full_simp_tac); |
476 Scan.succeed asm_full_simp_tac); |
477 |
477 |
478 fun simp_flags x = (Scan.repeat |
478 fun simp_flags x = (Scan.repeat |
479 (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat) |
479 (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat) |
480 >> setmp MetaSimplifier.simp_depth_limit) |
480 >> setmp MetaSimplifier.simp_depth_limit) |
481 >> curry (Library.foldl op o) I) x; |
481 >> (curry (Library.foldl op o) I o rev)) x; |
482 |
482 |
483 val cong_modifiers = |
483 val cong_modifiers = |
484 [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier), |
484 [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier), |
485 Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local), |
485 Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local), |
486 Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)]; |
486 Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)]; |