equal
deleted
inserted
replaced
338 (nat --| $$$ "-" -- nat >> PureThy.FromTo || |
338 (nat --| $$$ "-" -- nat >> PureThy.FromTo || |
339 nat --| $$$ "-" >> PureThy.From || |
339 nat --| $$$ "-" >> PureThy.From || |
340 nat >> PureThy.Single)); |
340 nat >> PureThy.Single)); |
341 |
341 |
342 val bang_facts = Scan.peek (fn context => |
342 val bang_facts = Scan.peek (fn context => |
343 $$$ "!" >> K (Assumption.prems_of (Context.proof_of context)) || Scan.succeed []); |
343 $$$ "!" >> (fn _ => (warning "use of prems in proof method"; |
|
344 Assumption.prems_of (Context.proof_of context))) || Scan.succeed []); |
344 |
345 |
345 |
346 |
346 (* goal specification *) |
347 (* goal specification *) |
347 |
348 |
348 (* range *) |
349 (* range *) |