|
|
8b3b135184
|
Fix Undo try
|
2024-05-20 15:03:50 +02:00 |
|
Marwan
|
075aa267a7
|
tests de l'alpha équiv, commentaire de mon code
|
2024-05-19 20:44:07 +02:00 |
|
Marwan
|
d3dcebdb88
|
renommage des tactiques, implémentation de la tactique try, suppression des tokens inutiles, etc..
|
2024-05-17 14:14:28 +02:00 |
|
Marwan
|
b1ccb0ad71
|
on force l'annotation sur le OU
|
2024-05-17 08:10:26 +02:00 |
|
|
|
b26ea09640
|
Split proof.ml with hlam.ml
|
2024-05-16 12:38:45 +02:00 |
|
Marwan
|
00c1a116d1
|
tactique apply généralisée, à commenter
|
2024-05-14 15:55:36 +02:00 |
|
|
|
84304e26dc
|
Fix and & or
|
2024-05-14 15:23:44 +02:00 |
|
Marwan
|
5ecf82920f
|
début de correction d'apply généralisé
|
2024-05-14 11:41:45 +02:00 |
|
Marwan
|
52ecb564fb
|
apply généralisé
|
2024-05-13 18:11:57 +02:00 |
|
|
|
daa09cb58b
|
Add Qed.
|
2024-05-13 18:05:28 +02:00 |
|
|
|
8569fe1ba2
|
Add Undo command
|
2024-05-11 11:44:43 +02:00 |
|
Marwan
|
5f28463a37
|
e doit typecheck dans exact e pour que la tactique réussisse
|
2024-05-06 13:21:33 +02:00 |
|
|
|
6251bb0b64
|
Add tactic split
|
2024-05-06 10:09:40 +02:00 |
|
|
|
24f78f58cd
|
Add tactics left and right
|
2024-05-05 20:45:55 +02:00 |
|
|
|
0085a91251
|
Better errors & add colors
|
2024-05-01 11:07:40 +02:00 |
|
|
|
fc846d2233
|
Add tactic intros
|
2024-05-01 10:44:36 +02:00 |
|
Marwan
|
20d4ee5531
|
on différencie exact pour les preuves et pour les termes
|
2024-04-30 11:56:41 +02:00 |
|
Marwan
|
ced6846dbc
|
tactique try et intro
|
2024-04-30 11:48:26 +02:00 |
|
|
|
6063d33377
|
Add interactive proofs
|
2024-04-30 11:44:28 +02:00 |
|
Marwan
|
7195fc244f
|
ajout du système de preuve et implémentation des tactiques exact, intro, cut et apply
|
2024-04-25 10:11:08 +02:00 |
|
