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
/
scratch.thy
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Test theories
Josh Chen
2018-08-18
1
-9
/
+0
*
Rename to distinguish function and path composition; function composition pro...
Josh Chen
2018-08-15
1
-72
/
+0
*
Well-formation rules are back in the methods; new theory synthesizing the nat...
Josh Chen
2018-08-14
1
-89
/
+69
*
rcompose done
Josh Chen
2018-08-13
1
-33
/
+16
*
Commit before testing polymorphic equality eliminator
Josh Chen
2018-08-12
1
-0
/
+6
*
Tweaks
Josh Chen
2018-08-07
1
-0
/
+6
*
Old application syntax incompatible with Eisbach
Josh Chen
2018-08-07
1
-2
/
+2
*
Partway through changing function application syntax style.
Josh Chen
2018-08-06
1
-98
/
+94
*
Unit and Null types. Methods.
Josh Chen
2018-07-12
1
-16
/
+34
*
Pre-universe implementation commit
Josh Chen
2018-07-09
1
-20
/
+51
*
Added attributes to type elimination rules, not sure if these will actually b...
Josh Chen
2018-07-06
1
-1
/
+54
*
Refactor HoTT_Methods.thy, proved more stuff with new methods.
Josh Chen
2018-07-03
1
-18
/
+2
*
Decided on a new proper scheme for type rules using the idea of implicit well...
Josh Chen
2018-06-17
1
-0
/
+24