1.1 --- a/doc-src/IsarRef/isar-ref.tex	Sun May 21 14:32:47 2000 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Sun May 21 14:33:46 2000 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  \makeindex
     1.6  
     1.7 -\railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
     1.8 +\railterm{percent,ppercent,underscore}
     1.9  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
    1.10  \railterm{name,nameref,text,type,term,prop,atom}
    1.11  

     2.1 --- a/doc-src/IsarRef/pure.tex	Sun May 21 14:32:47 2000 +0200
     2.2 +++ b/doc-src/IsarRef/pure.tex	Sun May 21 14:33:46 2000 +0200
     2.3 @@ -911,7 +911,7 @@
     2.4  
     2.5  \subsection{Block structure}
     2.6  
     2.7 -\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
     2.8 +\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}}
     2.9  \begin{matharray}{rcl}
    2.10    \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
    2.11    \BG & : & \isartrans{proof(state)}{proof(state)} \\
    2.12 @@ -933,9 +933,8 @@
    2.13  \begin{descr}
    2.14  \item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
    2.15    local context to the initial one.
    2.16 -\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
    2.17 -  close blocks.  Any current facts pass through ``$\isarkeyword{\{\{}$''
    2.18 -  unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
    2.19 +\item [$\BG$ and $\EN$] explicitly open and close blocks.  Any current facts
    2.20 +  pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be
    2.21    \emph{exported} into the enclosing context.  Thus fixed variables are
    2.22    generalized, assumptions discharged, and local definitions unfolded (cf.\ 
    2.23    \S\ref{sec:proof-context}).  There is no difference of $\ASSUMENAME$ and

     3.1 --- a/doc-src/IsarRef/syntax.tex	Sun May 21 14:32:47 2000 +0200
     3.2 +++ b/doc-src/IsarRef/syntax.tex	Sun May 21 14:33:46 2000 +0200
     3.3 @@ -139,15 +139,17 @@
     3.4  
     3.5  \subsection{Type classes, sorts and arities}
     3.6  
     3.7 -The syntax of sorts and arities is given directly at the outer level.  Note
     3.8 -that this is in contrast to types and terms (see \ref{sec:types-terms}).
     3.9 +Classes are specified by plain names.  Sorts have a very simple inner syntax,
    3.10 +which is either a single class name $c$ or a list $\{c@1, \dots, c@n\}$
    3.11 +referring to the intersection of these classes.  The syntax of type arities is
    3.12 +given directly at the outer level.
    3.13  
    3.14  \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
    3.15  \indexouternonterm{classdecl}
    3.16  \begin{rail}
    3.17    classdecl: name ('<' (nameref + ','))?
    3.18    ;
    3.19 -  sort: nameref | lbrace (nameref * ',') rbrace
    3.20 +  sort: nameref
    3.21    ;
    3.22    arity: ('(' (sort + ',') ')')? sort
    3.23    ;
    3.24 @@ -252,7 +254,7 @@
    3.25  \begin{rail}
    3.26    atom: nameref | typefree | typevar | var | nat | keyword
    3.27    ;
    3.28 -  arg: atom | '(' args ')' | '[' args ']' | lbrace args rbrace
    3.29 +  arg: atom | '(' args ')' | '[' args ']'
    3.30    ;
    3.31    args: arg *
    3.32    ;

     4.1 --- a/src/Pure/Isar/args.ML	Sun May 21 14:32:47 2000 +0200
     4.2 +++ b/src/Pure/Isar/args.ML	Sun May 21 14:33:46 2000 +0200
     4.3 @@ -181,7 +181,6 @@
     4.4    ((Scan.repeat1
     4.5      (Scan.repeat1 (atom_arg blk) ||
     4.6        paren_args "(" ")" args ||
     4.7 -      paren_args "{" "}" args ||
     4.8        paren_args "[" "]" args)) >> flat) x;
     4.9  
    4.10  

     5.1 --- a/src/Pure/Isar/isar_syn.ML	Sun May 21 14:32:47 2000 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun May 21 14:33:46 2000 +0200
     5.3 @@ -348,11 +348,11 @@
     5.4  (* proof structure *)
     5.5  
     5.6  val beginP =
     5.7 -  OuterSyntax.command "{{" "begin explicit proof block" K.prf_block
     5.8 +  OuterSyntax.command "{" "begin explicit proof block" K.prf_block
     5.9      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
    5.10  
    5.11  val endP =
    5.12 -  OuterSyntax.command "}}" "end explicit proof block" K.prf_block
    5.13 +  OuterSyntax.command "}" "end explicit proof block" K.prf_block
    5.14      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.end_block));
    5.15  
    5.16  val nextP =
    5.17 @@ -630,7 +630,7 @@
    5.18  val keywords =
    5.19   ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
    5.20    "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
    5.21 -  "files", "in", "infixl", "infixr", "is", "output", "{", "|", "}"];
    5.22 +  "files", "in", "infixl", "infixr", "is", "output", "|"];
    5.23  
    5.24  val parsers = [
    5.25    (*theory structure*)

     6.1 --- a/src/Pure/Thy/latex.ML	Sun May 21 14:32:47 2000 +0200
     6.2 +++ b/src/Pure/Thy/latex.ML	Sun May 21 14:33:46 2000 +0200
     6.3 @@ -76,8 +76,8 @@
     6.4        let val s = T.val_of tok in
     6.5          if invisible_token tok then ""
     6.6          else if T.is_kind T.Command tok then
     6.7 -          if s = "{{" then "{\\isabeginblock}"
     6.8 -          else if s = "}}" then "{\\isaendblock}"
     6.9 +          if s = "{" then "{\\isabeginblock}"
    6.10 +          else if s = "}" then "{\\isaendblock}"
    6.11            else "\\isacommand{" ^ output_syms s ^ "}"
    6.12          else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
    6.13            "\\isakeyword{" ^ output_syms s ^ "}"