words.input revision 51f82ef4ff2a9352e86e6dd35c7702f9e9382174
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichnand arch as assoc axiom axioms closed comm def else end
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichexists false fit forall free from generated get given
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichhide idem if in lambda library local not op ops pred preds
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichresult reveal sort sorts spec then to true type types
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichunit units var vars version view when with within ~
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%section: keyword
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%pattern: \textbf{%s}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichand arch as assoc axiom axioms closed comm def else end
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichexists false fit forall free from generated get given
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichhide idem if in lambda library local not op ops pred preds
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichresult reveal sort sorts spec then to true type types
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichunit units var vars version view when with within ~
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luetticha b c d e f g h i j k l m n o p q r s t u v w x y z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus LuettichA B C D E F G H I J K L M N O P Q R S T U V W X Y Z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%section: normal
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luetticha b c d e f g h i j k l m n o p q r s t u v w x y z � � � �
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichff fi fl ll Wo Wi Wa We Wu Po it Yo Ye Ya Yu Vo Ve Va Vi Vu ~ \_
96671d31fef5b34c14c938bd13f2495904574cd8Klaus LuettichA B C D E F G H I J K L M N O P Q R S T U V W X Y Z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich1 2 3 4 5 6 7 8 9 0 . "` "' `` '' ! , ; ? \textbar \textbackslash{} : ' / `
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich{\tt{}\textquotedblright}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich[ ] \{ \} ( ) \^{} \~{} \$
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%section: comment
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%pattern: {\small %s}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luetticha b c d e f g h i j k l m n o p q r s t u v w x y z � � � �
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichff fi fl ll Wo Wi Wa We Wu Po it Yo Ye Ya Yu Vo Ve Va Vi Vu ~ \_
96671d31fef5b34c14c938bd13f2495904574cd8Klaus LuettichA B C D E F G H I J K L M N O P Q R S T U V W X Y Z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich1 2 3 4 5 6 7 8 9 0 . "` "' `` '' ! , ; ? : ` '
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich[ ] \{ \} ( ) \^{} \~{} @ - = \{ \} | > < \textbackslash{} \$ *
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich{\tt{}\textquotedblright}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%section: structid
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%pattern: \textsc{%s}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luetticha b c d e f g h i j k l m n o p q r s t u v w x y z � � � �
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichpi ff fi fl ll Wo ~ \_ Po ow
96671d31fef5b34c14c938bd13f2495904574cd8Klaus LuettichA B C D E F G H I J K L M N O P Q R S T U V W X Y Z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich1 2 3 4 5 6 7 8 9 0 . /
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%section: annotation
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%pattern: {\small \textit{%s}}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luetticha b c d e f g h i j k l m n o p q r s t u v w x y z � � � � \_ , ; ? !
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichpi ff fi fl ll Wo Wi Wa We Wu Po it Yo Ye Ya Yu Vo Ve Va Vi Vu Mo
96671d31fef5b34c14c938bd13f2495904574cd8Klaus LuettichA B C D E F G H I J K L M N O P Q R S T U V W X Y Z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich\^{} \~{} / \% @ \textbackslash{} \$ :
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%pattern: {\small $%s$}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich1 2 3 4 5 6 7 8 9 0 . "` "' `` '' ~
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich\times * + - / < <> = >
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%section: annotationbf
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%pattern: {\small \textbf{%s}}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luetticha b c d e f g h i j k l m n o p q r s t u v w x y z � � � � \_ , ; ? !
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettichpi ff fi fl ll Wo Wi Wa We Wu Po it Yo Ye Ya Yu Vo Ve Va Vi Vu Mo
96671d31fef5b34c14c938bd13f2495904574cd8Klaus LuettichA B C D E F G H I J K L M N O P Q R S T U V W X Y Z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich� � � \% ( ) \{ \}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%section: axiom
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%pattern: $%s$
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich1 2 3 4 5 6 7 8 9 0 . `` '' ~ \_ \# | , : ; ? ! + - * / = < >
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich[ ] \{ \} ( ) ` ' @
51f82ef4ff2a9352e86e6dd35c7702f9e9382174Christian Maeder\bullet \Leftrightarrow \Rightarrow \Leftarrow \forall \exists \exists!
51f82ef4ff2a9352e86e6dd35c7702f9e9382174Christian Maeder\rightarrow \rightarrow? \leftarrow \neg \vee \wedge \in \mapsto \times
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich\leq \geq \cap \cup \subseteq \sim \sqcup \sqcap \bot \sharp
51f82ef4ff2a9352e86e6dd35c7702f9e9382174Christian Maeder\epsilon \longrightarrow \longleftarrow ^{-1}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich%pattern: \textit{%s}
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luetticha b c d e f g h i j k l m n o p q r s t u v w x y z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus LuettichA B C D E F G H I J K L M N O P Q R S T U V W X Y Z
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich"` "' � � � � � � �
96671d31fef5b34c14c938bd13f2495904574cd8Klaus Luettich\^{} \~{} \textbackslash{} \$ \% \&