index
:
Isabelle-HoTT
master
trying to make Isabelle/HoTT work with Isabelle 2021-1
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
mltt
/
core
/
goals.ML
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2021-06-24
Bad practice huge commit:
Josh Chen
1
-35
/
+66
2021-06-23
1. Put universe level parameters first in automatic term definitions. 2. Add ...
Josh Chen
1
-4
/
+5
2021-01-31
rename things + some small changes
Josh Chen
1
-0
/
+0
2020-08-14
(FEAT) Context data slots for known types and conditional type rules, as well...
Josh Chen
1
-3
/
+4
2020-07-31
(REF) Tweak attribute names in preparation for new logical introduction rule ...
Josh Chen
1
-1
/
+1
2020-07-31
(FEAT) Term elaboration of assumption and goal statements.
Josh Chen
1
-5
/
+5
2020-07-28
New `assuming` proof command for elaborated assumptions
Josh Chen
1
-1
/
+1
2020-07-27
Hook elaboration into assumptions mechanism
Josh Chen
1
-1
/
+1
2020-07-23
minor
Josh Chen
1
-67
/
+56
2020-07-08
1. Initial `Definition` keyword. 2. ifelse.
Josh Chen
1
-0
/
+9
2020-06-19
reorganize
Josh Chen
1
-0
/
+0
2020-05-28
reorganize folder structure
Josh Chen
1
-0
/
+0
2020-05-25
Reorganize theory structure. In particular, the identity type moves out from ...
Josh Chen
1
-0
/
+0
2020-04-16
update for Isabelle2020
Josh Chen
1
-1
/
+1
2020-04-02
Brand-spanking new version using Spartan infrastructure
Josh Chen
1
-0
/
+214