doc-src/TutorialI/Datatype/document/Fundata.tex
changeset 9145 9f7b8de5bfaf
parent 8771 026f37a86ea7
child 9541 d17c0b34d5c8
equal deleted inserted replaced
9144:20a70ef9c320 9145:9f7b8de5bfaf
    44 ~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
    44 ~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
    45 ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
    45 ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
    46 \end{isabellepar}%%
    46 \end{isabellepar}%%
    47 \end{isamarkuptext}%
    47 \end{isamarkuptext}%
    48 \end{isabelle}%
    48 \end{isabelle}%
       
    49 %%% Local Variables:
       
    50 %%% mode: latex
       
    51 %%% TeX-master: "root"
       
    52 %%% End: