# HG changeset patch
# User wenzelm
# Date 958913368 -7200
# Node ID a705822f4e2a05bf2f7cfd5d92b4747d1f377eed
# Parent  e591fc327675948ecbabb5455d8569f303eec143
replaced {{ }} by { };

diff -r e591fc327675 -r a705822f4e2a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Divides.thy	Sun May 21 14:49:28 2000 +0200
@@ -8,13 +8,13 @@
 
 Divides = Arith +
 
-(*We use the same sort for div and mod;
+(*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)
 axclass
   div < term
 
 instance
-  nat :: {div}
+  nat :: div
 
 consts
   div  :: ['a::div, 'a]  => 'a          (infixl 70)
diff -r e591fc327675 -r a705822f4e2a src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Sun May 21 14:49:28 2000 +0200
@@ -53,7 +53,7 @@
                   else         negateSnd (posDivAlg (-a,-b))"
 
 instance
-  int :: {div}
+  int :: "Divides.div"        (*avoid clash with 'div' token*)
 
 defs
   div_def   "a div b == fst (divAlg (a,b))"
diff -r e591fc327675 -r a705822f4e2a src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Sun May 21 14:49:28 2000 +0200
@@ -228,12 +228,12 @@
 
 lemma "A & B --> B & A";
 proof -;
-  {{;
+  {;
     assume ab: "A & B";
     from ab; have a: A; ..;
     from ab; have b: B; ..;
     from b a; have "B & A"; ..;
-  }};
+  };
   thus ?thesis; ..         -- {* rule \name{impI} *};
 qed;
 
diff -r e591fc327675 -r a705822f4e2a src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sun May 21 14:49:28 2000 +0200
@@ -49,19 +49,19 @@
   assume mono: "mono f";
   show "f ?a = ?a";
   proof -;
-    {{;
+    {;
       fix x;
       assume H: "x : ?H";
       hence "?a <= x"; by (rule Inter_lower);
       with mono; have "f ?a <= f x"; ..;
       also; from H; have "... <= x"; ..;
       finally; have "f ?a <= x"; .;
-    }};
+    };
     hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
-    {{;
+    {;
       also; presume "... <= f ?a";
       finally (order_antisym); show ?thesis; .;
-    }};
+    };
     from mono ge; have "f (f ?a) <= f ?a"; ..;
     hence "f ?a : ?H"; ..;
     thus "?a <= f ?a"; by (rule Inter_lower);
diff -r e591fc327675 -r a705822f4e2a src/HOL/Isar_examples/MultisetOrder.thy
--- a/src/HOL/Isar_examples/MultisetOrder.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Sun May 21 14:49:28 2000 +0200
@@ -67,7 +67,7 @@
 proof;
   let ?R = "mult1 r";
   let ?W = "acc ?R";
-  {{;
+  {;
     fix M M0 a;
     assume M0: "M0 : ?W"
       and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
@@ -110,7 +110,7 @@
 	thus "N : ?W"; by (simp only: N);
       qed;
     qed;
-  }}; note tedious_reasoning = this;
+  }; note tedious_reasoning = this;
 
   assume wf: "wf r";
   fix M;
diff -r e591fc327675 -r a705822f4e2a src/HOL/Isar_examples/Puzzle.thy
--- a/src/HOL/Isar_examples/Puzzle.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy	Sun May 21 14:49:28 2000 +0200
@@ -23,7 +23,7 @@
   (is "(!!x. ?H x ==> ?C x) ==> _");
 proof -;
   assume asm: "!!x. ?H x ==> ?C x";
-  {{;
+  {;
     fix k;
     have "ALL x. k = f x --> ?C x" (is "?Q k");
     proof (rule less_induct);
@@ -38,7 +38,7 @@
 	qed;
       qed;
     qed;
-  }};
+  };
   thus "?C x"; by simp;
 qed;
 
diff -r e591fc327675 -r a705822f4e2a src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Sun May 21 14:49:28 2000 +0200
@@ -48,7 +48,7 @@
 txt {* Define $M$ as the set of all norm-preserving extensions of $F$.  *};
 
   def M == "norm_pres_extensions E p F f";
-  {{;
+  {;
     fix c; assume "c : chain M" "EX x. x:c";
 
 txt {* Show that every non-empty chain $c$ in $M$ has an upper bound in $M$: $\Union c$ is greater that every element of the chain $c$, so $\Union c$ is an upper bound of $c$ that lies in $M$. *};
@@ -82,7 +82,7 @@
           by (rule sup_norm_pres [OF _ _ a]) (simp!)+;
       qed;
     qed;
-  }};
+  };
   
 txt {* With Zorn's Lemma we can conclude that there is a maximal element $g$ in $M$. *};
 
@@ -340,7 +340,7 @@
   It is even the least upper bound, because every upper bound of $M$
   is also an upper bound for $\Union c$, as $\Union c\in M$) *};
 
-  {{;
+  {;
     fix c; assume "c:chain M" "EX x. x:c";
     have "Union c : M";
 
@@ -372,7 +372,7 @@
           by (rule sup_norm_pres, rule a) (simp!)+;
       qed;
     qed;
-  }};
+  };
  
   txt {* According to Zorn's Lemma there is
   a maximal norm-preserving extension $g\in M$. *};