equal
deleted
inserted
replaced
557 val options_syntax = |
557 val options_syntax = |
558 (Args.parens (Args.$$$ "asm") >> (K true)) || |
558 (Args.parens (Args.$$$ "asm") >> (K true)) || |
559 (Scan.succeed false); |
559 (Scan.succeed false); |
560 |
560 |
561 val ith_syntax = |
561 val ith_syntax = |
562 (Args.parens (Scan.repeat Args.nat)) |
562 Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0]; |
563 || (Scan.succeed [0]); |
|
564 |
563 |
565 (* combination method that takes a flag (true indicates that subst |
564 (* combination method that takes a flag (true indicates that subst |
566 should be done to an assumption, false = apply to the conclusion of |
565 should be done to an assumption, false = apply to the conclusion of |
567 the goal) as well as the theorems to use *) |
566 the goal) as well as the theorems to use *) |
568 fun subst_meth src = |
567 fun subst_meth src = |