aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy
diff options
context:
space:
mode:
authorJosh Chen2018-07-04 10:50:52 +0200
committerJosh Chen2018-07-04 10:50:52 +0200
commitb65450369f992171f166a53e9cab408819cd987f (patch)
tree6c8449d762d26d68f9e4760a05520346eac5125a /Prod.thy
parent7823d59b2d9436f1bf0042fff62ee2bcc4c29ec0 (diff)
Trivial changes
Diffstat (limited to 'Prod.thy')
-rw-r--r--Prod.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Prod.thy b/Prod.thy
index 18582a8..7155a10 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -64,7 +64,7 @@ lemmas Prod_form_conds [elim, wellform] = Prod_form_cond1 Prod_form_cond2
text "Nondependent functions are a special case."
abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40)
- where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"
+ where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"
end \ No newline at end of file