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
/
Proj.thy
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2018-07-03
Refactor HoTT_Methods.thy, proved more stuff with new methods.
Josh Chen
1
-74
/
+30
2018-07-03
Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...
Josh Chen
1
-27
/
+6
2018-06-30
Finished proofs of projections
Josh Chen
1
-20
/
+76
2018-06-28
Proving theorems in Proj.thy in a simpler way with wellformed
Josh Chen
1
-40
/
+23
2018-06-27
Move projection function definitions out of Sum.thy
Josh Chen
1
-61
/
+27
2018-06-18
Dependent projection properties done.
Josh Chen
1
-27
/
+58
2018-06-18
Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...
Josh Chen
1
-16
/
+81
2018-06-18
Removed all [simp] attributes, these will be added later when I set up the si...
Josh Chen
1
-18
/
+31
2018-06-17
Proof of projection functions now harder. Should look up automation methods.
Josh Chen
1
-8
/
+14
2018-06-17
Eliminators must be completely parametrized at the meta-level.
Josh Chen
1
-14
/
+5
2018-06-15
projections
Josh Chen
1
-13
/
+28
2018-06-12
Type rules now have \"all\" premises explicitly stated, matching the formulat...
Josh Chen
1
-31
/
+62
2018-06-09
Reorganize code
Josh Chen
1
-0
/
+78