diff options
author | Josh Chen | 2018-07-03 18:57:57 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-03 18:57:57 +0200 |
commit | 7823d59b2d9436f1bf0042fff62ee2bcc4c29ec0 (patch) | |
tree | e45df70f36abdedfa0e5c2bcaebfb11022b18a41 /Sum.thy | |
parent | 9ffa5ed2a972db4ae6274a7852de37945a32ab0e (diff) |
Refactor HoTT_Methods.thy, proved more stuff with new methods.
Diffstat (limited to '')
-rw-r--r-- | Sum.thy | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -59,10 +59,10 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) lemma Pair_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : A \<times> B" -proof - fix b B assume "b : B" - then show "B : U" .. -qed + proof + fix b B assume "b : B" + then show "B : U" .. + qed end
\ No newline at end of file |