From 3cc293070ea306d3b9dc5c007267c5a8ad3c860e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 27 Dec 2011 13:16:22 +0000 Subject: Add big Integral --- etc/isar/TokensAcid.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'etc') 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 \ \ \\<^ebig>" +term "\<^bbig>large text \ \ \ \\<^ebig>" term "\<^bsmall>smaller text ((\ \ \) \ \) \<^esmall>" -- cgit v1.2.3