From 5066281145a541203ecb56407131e98e4e70d2ec Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Fri, 2 Aug 2019 20:10:38 +0100 Subject: [PATCH] Fixed index de-reference for outer syntax. --- examples/technical_report/Isabelle_DOF-Manual/02_Background.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index 1d32db9f..a1f664d9 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -76,7 +76,7 @@ text\ separate commands from each other. We distinguish fundamentally two different syntactic levels: - \<^item> the \emph{outer-syntax}\bindex{syntax!outer}\index{outer syntax|see {syntax, inner}} (\ie, the + \<^item> the \emph{outer-syntax}\bindex{syntax!outer}\index{outer syntax|see {syntax, outer}} (\ie, the syntax for commands) is processed by a lexer-library and parser combinators built on top, and \<^item> the \emph{inner-syntax}\bindex{syntax!inner}\index{inner syntax|see {syntax, inner}} (\ie, the syntax for \inlineisar|\|-terms in HOL) with its own parametric polymorphism type