src/Pure/Isar/isar_syn.ML
changeset 8896 c80aba8c1d5e
parent 8886 111476895bf2
child 8966 916966f68907
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun May 21 14:32:47 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun May 21 14:33:46 2000 +0200
     1.3 @@ -348,11 +348,11 @@
     1.4  (* proof structure *)
     1.5  
     1.6  val beginP =
     1.7 -  OuterSyntax.command "{{" "begin explicit proof block" K.prf_block
     1.8 +  OuterSyntax.command "{" "begin explicit proof block" K.prf_block
     1.9      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
    1.10  
    1.11  val endP =
    1.12 -  OuterSyntax.command "}}" "end explicit proof block" K.prf_block
    1.13 +  OuterSyntax.command "}" "end explicit proof block" K.prf_block
    1.14      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.end_block));
    1.15  
    1.16  val nextP =
    1.17 @@ -630,7 +630,7 @@
    1.18  val keywords =
    1.19   ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
    1.20    "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
    1.21 -  "files", "in", "infixl", "infixr", "is", "output", "{", "|", "}"];
    1.22 +  "files", "in", "infixl", "infixr", "is", "output", "|"];
    1.23  
    1.24  val parsers = [
    1.25    (*theory structure*)