aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-12-27 13:16:22 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-12-27 13:16:22 +0000
commit3cc293070ea306d3b9dc5c007267c5a8ad3c860e (patch)
tree7403b7eb54771864f76cc0694b79e7f7e942949a /etc
parente388da31dddc2f2b99935b9ef6a064c088a91894 (diff)
Add big Integral
Diffstat (limited to 'etc')
-rw-r--r--etc/isar/TokensAcid.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy
index 9b0e38af..8b37d951 100644
--- a/etc/isar/TokensAcid.thy
+++ b/etc/isar/TokensAcid.thy
@@ -186,7 +186,7 @@ notation (xsymbols)
underline ("\<^bunderline>_\<^eunderline>") and
overline ("\<^boverline>_\<^eoverline>")
-term "\<^bbig>large text \<alpha> \<beta> \<Sigma>\<^ebig>"
+term "\<^bbig>large text \<alpha> \<beta> \<Sigma> \<integral>\<^ebig>"
term "\<^bsmall>smaller text ((\<alpha> \<and> \<beta>) \<longrightarrow> \<gamma>) \<^esmall>"