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
/
Nat.thy
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...
Josh Chen
2018-09-18
1
-0
/
+1
*
Reorganizing theories
Josh Chen
2018-09-17
1
-33
/
+27
*
Reorganized HoTT_Base, updated theories
Josh Chen
2018-09-16
1
-18
/
+18
|
\
|
*
Go back to higher-order application notation
Josh Chen
2018-09-11
1
-14
/
+14
|
/
*
Reorganize methods
Josh Chen
2018-08-18
1
-1
/
+1
*
Regrouping type rules
Josh Chen
2018-08-18
1
-10
/
+9
*
Cleanups
Josh Chen
2018-08-17
1
-4
/
+4
*
Prod.thy now has the correct definitional equality structure rule. Definition...
Josh Chen
2018-08-16
1
-1
/
+1
*
Well-formation rules are back in the methods; new theory synthesizing the nat...
Josh Chen
2018-08-14
1
-0
/
+5
*
Equality inverse and composition done. Cleaned up methods and method example ...
Josh Chen
2018-08-14
1
-1
/
+1
*
rcompose done
Josh Chen
2018-08-13
1
-0
/
+1
*
Old application syntax incompatible with Eisbach
Josh Chen
2018-08-07
1
-15
/
+15
*
Partway through changing function application syntax style.
Josh Chen
2018-08-06
1
-0
/
+49
