Jon Eugster
|
3d9d4f1d54
|
14 month time-skip
|
2025-08-06 00:28:59 +02:00 |
|
Jon Eugster
|
2dde9482d2
|
bump to v4.7.0
|
2024-04-10 17:07:22 +02:00 |
|
Jon Eugster
|
c35d29dcf4
|
make simp_add available in the entire game #54
|
2024-03-18 16:21:49 +01:00 |
|
Jon Eugster
|
5010691770
|
remove ring tactic
|
2024-03-14 11:13:59 +01:00 |
|
Jon Eugster
|
d6bf5686bc
|
rename iGiveUpAx to xyzzyAxiom
|
2024-03-14 10:38:41 +01:00 |
|
Jon Eugster
|
1a66069e89
|
do not import all of mathlib
|
2024-03-14 10:38:03 +01:00 |
|
Jon Eugster
|
381a729f3e
|
bump to v4.6.0
|
2024-02-29 17:19:01 +01:00 |
|
Jon Eugster
|
30232f30e2
|
bump to v4.5.0
|
2024-02-20 14:54:21 +01:00 |
|
Kevin Buzzard
|
396a350bda
|
use mathlib Apply ... At
|
2024-01-23 19:24:42 +00:00 |
|
Kevin Buzzard
|
127ebffb6a
|
Replace recursive definitions of algebraic operations with axioms (#41)
change to axiom approach
|
2023-11-22 09:26:49 +01:00 |
|
joneugster
|
14ce186239
|
pretty-printer for not equal
|
2023-10-28 22:01:03 +02:00 |
|
joneugster
|
a851a29928
|
custom use tactic
|
2023-10-28 11:48:49 +02:00 |
|
Kevin Buzzard
|
cedc46846d
|
add mystical ancient tactic
|
2023-10-23 13:43:48 +01:00 |
|
joneugster
|
1dbfaae51c
|
the tactic of tactics
|
2023-10-15 03:17:30 +02:00 |
|
joneugster
|
3333a85d02
|
fix induction
|
2023-10-15 01:16:09 +02:00 |
|
Kevin Buzzard
|
8b805a800c
|
fix naming
|
2023-10-14 22:34:24 +01:00 |
|
joneugster
|
21a36dc8d5
|
custom cases tactic
|
2023-10-14 21:13:06 +02:00 |
|
Kevin Buzzard
|
3648e91933
|
fixes
|
2023-10-14 17:29:11 +01:00 |
|
Kevin Buzzard
|
f625cb5530
|
add not quite working cases.
|
2023-10-14 17:15:11 +01:00 |
|
Kevin Buzzard
|
bf013af673
|
Merge branch 'main' into level-rewrite
|
2023-10-11 17:58:40 +01:00 |
|
joneugster
|
dc5635b878
|
extend rfl to proof iff statement #18
|
2023-10-09 21:26:02 +02:00 |
|
Kevin Buzzard
|
0e36f7d8f7
|
apply at!
|
2023-10-04 15:43:57 +01:00 |
|
Kevin Buzzard
|
4e1330bb99
|
more advanced addition world
|
2023-10-02 18:59:47 +01:00 |
|
Jon Eugster
|
8c61ebab70
|
bump mathlib
|
2023-09-10 17:10:28 +02:00 |
|
Kevin Buzzard
|
3fb6d7113f
|
apply to -> apply at
|
2023-08-07 18:37:42 +01:00 |
|
Jon Eugster
|
5a9bb1c119
|
apply f to h
|
2023-08-06 23:45:04 +02:00 |
|
Jon Eugster
|
c80a695def
|
enable ac_rfl
|
2023-08-06 23:28:11 +02:00 |
|
Jon Eugster
|
836f8f6078
|
import Mathlib.Tactic everywhere
|
2023-08-04 17:14:49 +02:00 |
|
Jon Eugster
|
2604c89284
|
big refactor
|
2023-05-15 15:12:35 +02:00 |
|