# HG changeset patch
# User wenzelm
# Date 958912426 -7200
# Node ID c80aba8c1d5ecad2abfd5fe54201fed6a74fd9dc
# Parent  2913a54e64cf2b1fdc3e8b5febffa851754e796c
replaced {{ }} by { };

diff -r 2913a54e64cf -r c80aba8c1d5e doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Sun May 21 14:32:47 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Sun May 21 14:33:46 2000 +0200
@@ -9,7 +9,7 @@
 
 \makeindex
 
-\railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
+\railterm{percent,ppercent,underscore}
 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
 \railterm{name,nameref,text,type,term,prop,atom}
 
diff -r 2913a54e64cf -r c80aba8c1d5e doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sun May 21 14:32:47 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Sun May 21 14:33:46 2000 +0200
@@ -911,7 +911,7 @@
 
 \subsection{Block structure}
 
-\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
+\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}}
 \begin{matharray}{rcl}
   \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
   \BG & : & \isartrans{proof(state)}{proof(state)} \\
@@ -933,9 +933,8 @@
 \begin{descr}
 \item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
   local context to the initial one.
-\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
-  close blocks.  Any current facts pass through ``$\isarkeyword{\{\{}$''
-  unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
+\item [$\BG$ and $\EN$] explicitly open and close blocks.  Any current facts
+  pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be
   \emph{exported} into the enclosing context.  Thus fixed variables are
   generalized, assumptions discharged, and local definitions unfolded (cf.\ 
   \S\ref{sec:proof-context}).  There is no difference of $\ASSUMENAME$ and
diff -r 2913a54e64cf -r c80aba8c1d5e doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sun May 21 14:32:47 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sun May 21 14:33:46 2000 +0200
@@ -139,15 +139,17 @@
 
 \subsection{Type classes, sorts and arities}
 
-The syntax of sorts and arities is given directly at the outer level.  Note
-that this is in contrast to types and terms (see \ref{sec:types-terms}).
+Classes are specified by plain names.  Sorts have a very simple inner syntax,
+which is either a single class name $c$ or a list $\{c@1, \dots, c@n\}$
+referring to the intersection of these classes.  The syntax of type arities is
+given directly at the outer level.
 
 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
 \indexouternonterm{classdecl}
 \begin{rail}
   classdecl: name ('<' (nameref + ','))?
   ;
-  sort: nameref | lbrace (nameref * ',') rbrace
+  sort: nameref
   ;
   arity: ('(' (sort + ',') ')')? sort
   ;
@@ -252,7 +254,7 @@
 \begin{rail}
   atom: nameref | typefree | typevar | var | nat | keyword
   ;
-  arg: atom | '(' args ')' | '[' args ']' | lbrace args rbrace
+  arg: atom | '(' args ')' | '[' args ']'
   ;
   args: arg *
   ;
diff -r 2913a54e64cf -r c80aba8c1d5e src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sun May 21 14:32:47 2000 +0200
+++ b/src/Pure/Isar/args.ML	Sun May 21 14:33:46 2000 +0200
@@ -181,7 +181,6 @@
   ((Scan.repeat1
     (Scan.repeat1 (atom_arg blk) ||
       paren_args "(" ")" args ||
-      paren_args "{" "}" args ||
       paren_args "[" "]" args)) >> flat) x;
 
 
diff -r 2913a54e64cf -r c80aba8c1d5e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun May 21 14:32:47 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun May 21 14:33:46 2000 +0200
@@ -348,11 +348,11 @@
 (* proof structure *)
 
 val beginP =
-  OuterSyntax.command "{{" "begin explicit proof block" K.prf_block
+  OuterSyntax.command "{" "begin explicit proof block" K.prf_block
     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
 
 val endP =
-  OuterSyntax.command "}}" "end explicit proof block" K.prf_block
+  OuterSyntax.command "}" "end explicit proof block" K.prf_block
     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.end_block));
 
 val nextP =
@@ -630,7 +630,7 @@
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
-  "files", "in", "infixl", "infixr", "is", "output", "{", "|", "}"];
+  "files", "in", "infixl", "infixr", "is", "output", "|"];
 
 val parsers = [
   (*theory structure*)
diff -r 2913a54e64cf -r c80aba8c1d5e src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun May 21 14:32:47 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Sun May 21 14:33:46 2000 +0200
@@ -76,8 +76,8 @@
       let val s = T.val_of tok in
         if invisible_token tok then ""
         else if T.is_kind T.Command tok then
-          if s = "{{" then "{\\isabeginblock}"
-          else if s = "}}" then "{\\isaendblock}"
+          if s = "{" then "{\\isabeginblock}"
+          else if s = "}" then "{\\isaendblock}"
           else "\\isacommand{" ^ output_syms s ^ "}"
         else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
           "\\isakeyword{" ^ output_syms s ^ "}"