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
/
Prod.thy
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2018-08-15
Function composition, rename path composition to differentiate the two.
Josh Chen
1
-0
/
+16
2018-08-13
rcompose done
Josh Chen
1
-14
/
+8
2018-08-12
Commit before testing polymorphic equality eliminator
Josh Chen
1
-10
/
+12
2018-08-07
Old application syntax incompatible with Eisbach
Josh Chen
1
-6
/
+6
2018-08-07
Experiment with polymorphic dependent eliminators, i.e. we leave type and typ...
Josh Chen
1
-5
/
+5
2018-08-06
Partway through changing function application syntax style.
Josh Chen
1
-17
/
+17
2018-08-04
Reorganize theories
Josh Chen
1
-26
/
+30
2018-07-12
Unit and Null types. Methods.
Josh Chen
1
-0
/
+19
2018-07-11
Universes implemented. Type rules modified accordingly. No more automatic der...
Josh Chen
1
-4
/
+4
2018-07-07
Library snapshot. Methods written, everything nicely organized.
Josh Chen
1
-0
/
+1
2018-07-06
Remove extra attributes for elimination rules, unneeded for now.
Josh Chen
1
-2
/
+1
2018-07-06
Added attributes to type elimination rules, not sure if these will actually b...
Josh Chen
1
-0
/
+2
2018-07-04
Trivial changes
Josh Chen
1
-1
/
+1
2018-07-03
Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...
Josh Chen
1
-2
/
+1
2018-06-30
Proving path composition. Need to set up the Simplifier to simplify applicati...
Josh Chen
1
-0
/
+1
2018-06-30
Finished proofs of projections
Josh Chen
1
-1
/
+1
2018-06-18
Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...
Josh Chen
1
-5
/
+13
2018-06-18
Removed all [simp] attributes, these will be added later when I set up the si...
Josh Chen
1
-12
/
+19
2018-06-17
Decided on a new proper scheme for type rules using the idea of implicit well...
Josh Chen
1
-1
/
+1
2018-06-12
Type rules now have \"all\" premises explicitly stated, matching the formulat...
Josh Chen
1
-6
/
+13
2018-06-09
Reorganize code
Josh Chen
1
-0
/
+48