equal
deleted
inserted
replaced
434 type modifier = (Proof.context -> Proof.context) * attribute; |
434 type modifier = (Proof.context -> Proof.context) * attribute; |
435 |
435 |
436 local |
436 local |
437 |
437 |
438 fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; |
438 fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; |
439 fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths); |
439 fun app (f, att) (context, ths) = Library.foldl_map att (Context.map_proof f context, ths); |
440 |
440 |
441 fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- |
441 fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- |
442 (fn (m, ths) => Scan.succeed (app m (context, ths)))); |
442 (fn (m, ths) => Scan.succeed (app m (context, ths)))); |
443 |
443 |
444 fun sectioned args ss = args -- Scan.repeat (section ss); |
444 fun sectioned args ss = args -- Scan.repeat (section ss); |