diff options
| author | Lars Hupel | 2018-09-18 16:52:08 +0200 |
|---|---|---|
| committer | Lars Hupel | 2018-09-18 16:52:08 +0200 |
| commit | f07e0e2349a222130209ada9c029eea3d1fe8144 (patch) | |
| tree | df5863f0fe5dd181dde689383a101bf3bb3f57e5 | |
| parent | c93932c689640a530de946f35a0a9dc82e56e776 (diff) | |
add ROOT file
| -rw-r--r-- | EqualProps.thy | 1 | ||||
| -rw-r--r-- | ROOT | 10 | ||||
| -rw-r--r-- | ex/Book/Ch1.thy (renamed from ex/HoTT book/Ch1.thy) | 2 |
3 files changed, 11 insertions, 2 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index abb2623..f7a8d91 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -117,7 +117,6 @@ proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) fix x assume "x: A" show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r" \<comment> \<open>This requires substitution of *propositional* equality. \<close> - sorry oops @@ -0,0 +1,10 @@ +session HoTT = Pure + + sessions + "HOL-Eisbach" + theories + HoTT_Base + HoTT + "tests/Test" + "ex/Methods" + "ex/Synthesis" + "ex/Book/Ch1"
\ No newline at end of file diff --git a/ex/HoTT book/Ch1.thy b/ex/Book/Ch1.thy index 263f43d..dfb1879 100644 --- a/ex/HoTT book/Ch1.thy +++ b/ex/Book/Ch1.thy @@ -1,5 +1,5 @@ (* -Title: ex/HoTT book/Ch1.thy +Title: ex/Book/Ch1.thy Author: Josh Chen Date: 2018 |