src/Pure/Thy/html.scala
changeset 65771 688a7dd22cbb
parent 65753 787e5ee6ef53
child 65773 120ef768c84c
--- a/src/Pure/Thy/html.scala	Mon May 08 12:04:58 2017 +0200
+++ b/src/Pure/Thy/html.scala	Mon May 08 14:08:27 2017 +0200
@@ -103,6 +103,7 @@
   val par = new Operator("p")
   val emph = new Operator("em")
   val bold = new Operator("b")
+  val code = new Operator("code")
 
   val title = new Heading("title")
   val chapter = new Heading("h1")