replaced {{ }} by { };
authorwenzelm
Sun May 21 14:49:28 2000 +0200 (2000-05-21)
changeset 8902a705822f4e2a
parent 8901 e591fc327675
child 8903 78d6e47469e4
replaced {{ }} by { };
src/HOL/Divides.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Isar_examples/BasicLogic.thy
src/HOL/Isar_examples/KnasterTarski.thy
src/HOL/Isar_examples/MultisetOrder.thy
src/HOL/Isar_examples/Puzzle.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
     1.1 --- a/src/HOL/Divides.thy	Sun May 21 14:44:01 2000 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun May 21 14:49:28 2000 +0200
     1.3 @@ -8,13 +8,13 @@
     1.4  
     1.5  Divides = Arith +
     1.6  
     1.7 -(*We use the same sort for div and mod;
     1.8 +(*We use the same class for div and mod;
     1.9    moreover, dvd is defined whenever multiplication is*)
    1.10  axclass
    1.11    div < term
    1.12  
    1.13  instance
    1.14 -  nat :: {div}
    1.15 +  nat :: div
    1.16  
    1.17  consts
    1.18    div  :: ['a::div, 'a]  => 'a          (infixl 70)
     2.1 --- a/src/HOL/Integ/IntDiv.thy	Sun May 21 14:44:01 2000 +0200
     2.2 +++ b/src/HOL/Integ/IntDiv.thy	Sun May 21 14:49:28 2000 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4                    else         negateSnd (posDivAlg (-a,-b))"
     2.5  
     2.6  instance
     2.7 -  int :: {div}
     2.8 +  int :: "Divides.div"        (*avoid clash with 'div' token*)
     2.9  
    2.10  defs
    2.11    div_def   "a div b == fst (divAlg (a,b))"
     3.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sun May 21 14:44:01 2000 +0200
     3.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sun May 21 14:49:28 2000 +0200
     3.3 @@ -228,12 +228,12 @@
     3.4  
     3.5  lemma "A & B --> B & A";
     3.6  proof -;
     3.7 -  {{;
     3.8 +  {;
     3.9      assume ab: "A & B";
    3.10      from ab; have a: A; ..;
    3.11      from ab; have b: B; ..;
    3.12      from b a; have "B & A"; ..;
    3.13 -  }};
    3.14 +  };
    3.15    thus ?thesis; ..         -- {* rule \name{impI} *};
    3.16  qed;
    3.17  
     4.1 --- a/src/HOL/Isar_examples/KnasterTarski.thy	Sun May 21 14:44:01 2000 +0200
     4.2 +++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sun May 21 14:49:28 2000 +0200
     4.3 @@ -49,19 +49,19 @@
     4.4    assume mono: "mono f";
     4.5    show "f ?a = ?a";
     4.6    proof -;
     4.7 -    {{;
     4.8 +    {;
     4.9        fix x;
    4.10        assume H: "x : ?H";
    4.11        hence "?a <= x"; by (rule Inter_lower);
    4.12        with mono; have "f ?a <= f x"; ..;
    4.13        also; from H; have "... <= x"; ..;
    4.14        finally; have "f ?a <= x"; .;
    4.15 -    }};
    4.16 +    };
    4.17      hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
    4.18 -    {{;
    4.19 +    {;
    4.20        also; presume "... <= f ?a";
    4.21        finally (order_antisym); show ?thesis; .;
    4.22 -    }};
    4.23 +    };
    4.24      from mono ge; have "f (f ?a) <= f ?a"; ..;
    4.25      hence "f ?a : ?H"; ..;
    4.26      thus "?a <= f ?a"; by (rule Inter_lower);
     5.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Sun May 21 14:44:01 2000 +0200
     5.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy	Sun May 21 14:49:28 2000 +0200
     5.3 @@ -67,7 +67,7 @@
     5.4  proof;
     5.5    let ?R = "mult1 r";
     5.6    let ?W = "acc ?R";
     5.7 -  {{;
     5.8 +  {;
     5.9      fix M M0 a;
    5.10      assume M0: "M0 : ?W"
    5.11        and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
    5.12 @@ -110,7 +110,7 @@
    5.13  	thus "N : ?W"; by (simp only: N);
    5.14        qed;
    5.15      qed;
    5.16 -  }}; note tedious_reasoning = this;
    5.17 +  }; note tedious_reasoning = this;
    5.18  
    5.19    assume wf: "wf r";
    5.20    fix M;
     6.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Sun May 21 14:44:01 2000 +0200
     6.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Sun May 21 14:49:28 2000 +0200
     6.3 @@ -23,7 +23,7 @@
     6.4    (is "(!!x. ?H x ==> ?C x) ==> _");
     6.5  proof -;
     6.6    assume asm: "!!x. ?H x ==> ?C x";
     6.7 -  {{;
     6.8 +  {;
     6.9      fix k;
    6.10      have "ALL x. k = f x --> ?C x" (is "?Q k");
    6.11      proof (rule less_induct);
    6.12 @@ -38,7 +38,7 @@
    6.13  	qed;
    6.14        qed;
    6.15      qed;
    6.16 -  }};
    6.17 +  };
    6.18    thus "?C x"; by simp;
    6.19  qed;
    6.20  
     7.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Sun May 21 14:44:01 2000 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Sun May 21 14:49:28 2000 +0200
     7.3 @@ -48,7 +48,7 @@
     7.4  txt {* Define $M$ as the set of all norm-preserving extensions of $F$.  *};
     7.5  
     7.6    def M == "norm_pres_extensions E p F f";
     7.7 -  {{;
     7.8 +  {;
     7.9      fix c; assume "c : chain M" "EX x. x:c";
    7.10  
    7.11  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$. *};
    7.12 @@ -82,7 +82,7 @@
    7.13            by (rule sup_norm_pres [OF _ _ a]) (simp!)+;
    7.14        qed;
    7.15      qed;
    7.16 -  }};
    7.17 +  };
    7.18    
    7.19  txt {* With Zorn's Lemma we can conclude that there is a maximal element $g$ in $M$. *};
    7.20  
    7.21 @@ -340,7 +340,7 @@
    7.22    It is even the least upper bound, because every upper bound of $M$
    7.23    is also an upper bound for $\Union c$, as $\Union c\in M$) *};
    7.24  
    7.25 -  {{;
    7.26 +  {;
    7.27      fix c; assume "c:chain M" "EX x. x:c";
    7.28      have "Union c : M";
    7.29  
    7.30 @@ -372,7 +372,7 @@
    7.31            by (rule sup_norm_pres, rule a) (simp!)+;
    7.32        qed;
    7.33      qed;
    7.34 -  }};
    7.35 +  };
    7.36   
    7.37    txt {* According to Zorn's Lemma there is
    7.38    a maximal norm-preserving extension $g\in M$. *};