Hi list,
I developed a new tactic that takes a theorem of the form P == l = r and
replaces l by r in a goal adding whatever it needs to make it work properly
(typically conjunction with P; but can also be an implication or even
existentials).
This is a follow-up of the discussion I started a few
Hi Peter,
here is the difference:
(* The new hypotheses are added as conjuncts rather than as a *)
(* separate subgoal to reduce the user's burden of subgoal splits *)
(* when creating tactics to prove theorems. If a separate subgoal*)
(* is desired, simply use CONJ_TAC after
MCS Special Issue:
Formal Proofs for Mathematics and Computer Science
http://www-sop.inria.fr/marelle/MCS-FP-2013/
CALL FOR PAPERS
We invite submission of papers on Proof Formalization
for possible publication in this Mathematics in Computer
Science (MCS) special issue.
Deadlines:
Forgot: in the examples below, both tactics are used with the theorem |-
!x. x 0 == x / x = 1
2013/7/11 Vincent Aravantinos vincent.aravanti...@gmail.com
Hi Peter,
here is the difference:
(* The new hypotheses are added as conjuncts rather than as a *)
(* separate subgoal to
NFM Group,
This is a call for highlights for an article that I am writing. I would
very much like to feature developments in formal methods! Please
consider sending me a highlight on your work.
Cheers,
Kristin
=
Please circulate this reminder to your colleagues:
