equal
deleted
inserted
replaced
142 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline |
142 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline |
143 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline |
143 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline |
144 \isakeyword{monos}\ lists_mono |
144 \isakeyword{monos}\ lists_mono |
145 \end{isabelle} |
145 \end{isabelle} |
146 |
146 |
147 We must cite the theorem \isa{lists_mono} in order to justify |
147 We cite the theorem \isa{lists_mono} to justify |
148 using the function \isa{lists}. |
148 using the function \isa{lists}.% |
|
149 \footnote{This particular theorem is installed by default already, but we |
|
150 include the \isakeyword{monos} declaration in order to illustrate its syntax.} |
149 \begin{isabelle} |
151 \begin{isabelle} |
150 A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq |
152 A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq |
151 \ lists\ B\rulenamedx{lists_mono} |
153 \ lists\ B\rulenamedx{lists_mono} |
152 \end{isabelle} |
154 \end{isabelle} |
153 % |
155 % |