(*<*)+− theory Paper+− imports "~~/src/HOL/Library/LaTeXsugar" +− begin+− +− declare [[show_question_marks = false]]+− +− section {* Introduction *}+− +− text {*+− mention Russo paper which concludes that technology is not +− ready beyond core-calculi.+− +− +− +− *}+− +− +− (*<*)+− end+− (*>*)+−