David Raymond Christiansen c9973eb7c3 Add andThen and refine to Pruviloj ... andThen is a subgoal sequencing combinator, and refine is a bit like Coq's eapply.		2015-10-01 18:28:40 +02:00
..
expected	Library of tactics for proof automation with Elab	2015-09-25 13:24:42 +02:00
pruviloj001.idr	Add andThen and refine to Pruviloj	2015-10-01 18:28:40 +02:00
run	Library of tactics for proof automation with Elab	2015-09-25 13:24:42 +02:00