tuned;

--- a/src/HOL/Induct/Multiset.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Induct/Multiset.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -5,8 +5,6 @@
 
 A definitional theory of multisets,
 including a wellfoundedness proof for the multiset order.
-use_thy"Multiset";
-
 *)
 
 Multiset = Multiset0 + Acc +

--- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -221,7 +221,7 @@
 qed;
 
 text {*
- We can still push forward reasoning a bit further, even at the risk
+ We can still push forward-reasoning a bit further, even at the risk
  of getting ridiculous.  Note that we force the initial proof step to
  do nothing here, by referring to the ``-'' proof method.
 *};

--- a/src/HOL/Isar_examples/ExprCompiler.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -169,7 +169,8 @@
           exec (Const val # xs @ ys) s env";
         by simp;
       also; have "... = exec (xs @ ys) (val # s) env"; by simp;
-      also; from hyp; have "... = exec ys (exec xs (val # s) env) env"; ..;
+      also; from hyp;
+        have "... = exec ys (exec xs (val # s) env) env"; ..;
       also; have "... = exec ys (exec (Const val # xs) s env) env";
         by simp;
       finally; show "?Q s"; .;
@@ -188,7 +189,8 @@
           exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env";
         by simp;
       also; from hyp; have "... =
-        exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"; ..;
+        exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env";
+        ..;
       also; have "... = exec ys (exec (Apply fun # xs) s env) env"; by simp;
       finally; show "?Q s"; .;
     qed;
@@ -198,7 +200,8 @@
 theorem correctness: "execute (compile e) env = eval e env";
 proof -;
   have exec_compile:
-  "ALL stack. exec (compile e) stack env = eval e env # stack" (is "?P e");
+    "ALL stack. exec (compile e) stack env = eval e env # stack"
+    (is "?P e");
   proof (induct e);
     fix adr; show "?P (Variable adr)" (is "ALL s. ?Q s");
     proof;
@@ -217,15 +220,18 @@
     proof;
       fix s; have "exec (compile (Binop fun e1 e2)) s env
         = exec (compile e2 @ compile e1 @ [Apply fun]) s env"; by simp;
-      also; have "... =
-          exec [Apply fun] (exec (compile e1) (exec (compile e2) s env) env) env";
+      also; have "... = exec [Apply fun]
+          (exec (compile e1) (exec (compile e2) s env) env) env";
         by (simp only: exec_append);
-      also; from hyp2; have "exec (compile e2) s env = eval e2 env # s"; ..;
-      also; from hyp1; have "exec (compile e1) ... env = eval e1 env # ..."; ..;
+      also; from hyp2;
+        have "exec (compile e2) s env = eval e2 env # s"; ..;
+      also; from hyp1;
+        have "exec (compile e1) ... env = eval e1 env # ..."; ..;
       also; have "exec [Apply fun] ... env =
         fun (hd ...) (hd (tl ...)) # (tl (tl ...))"; by simp;
       also; have "... = fun (eval e1 env) (eval e2 env) # s"; by simp;
-      also; have "fun (eval e1 env) (eval e2 env) = eval (Binop fun e1 e2) env";
+      also; have "fun (eval e1 env) (eval e2 env) =
+          eval (Binop fun e1 e2) env";
         by simp;
       finally; show "?Q s"; .;
     qed;
@@ -233,7 +239,8 @@
 
   have "execute (compile e) env = hd (exec (compile e) [] env)";
     by (simp add: execute_def);
-  also; from exec_compile; have "exec (compile e) [] env = [eval e env]"; ..;
+  also; from exec_compile;
+    have "exec (compile e) [] env = [eval e env]"; ..;
   also; have "hd ... = eval e env"; by simp;
   finally; show ?thesis; .;
 qed;

--- a/src/HOL/Isar_examples/Fibonacci.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -39,7 +39,7 @@
 text {* Alternative induction rule. *};
 
 theorem fib_induct:
-"[| P 0; P 1; !!n. [| P (n + 1); P n |] ==> P (n + 2) |] ==> P n";
+    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P n";
   by (induct rule: fib.induct, simp+);
 
 
@@ -48,10 +48,11 @@
 
 text {* A few laws taken from \cite{Concrete-Math}. *};
 
-lemma fib_add: 
+lemma fib_add:
   "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
-  (is "?P n");
-proof (induct ?P n rule: fib_induct) -- {* see \cite[page 280]{Concrete-Math} *};
+  (is "?P n")
+  -- {* see \cite[page 280]{Concrete-Math} *};
+proof (induct ?P n rule: fib_induct);
   show "?P 0"; by simp;
   show "?P 1"; by simp;
   fix n;
@@ -70,11 +71,11 @@
 qed;
 
 lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n");
-proof (induct ?P n rule: fib_induct); 
+proof (induct ?P n rule: fib_induct);
   show "?P 0"; by simp;
   show "?P 1"; by simp;
-  fix n; 
-  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"; 
+  fix n;
+  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)";
     by simp;
   also; have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))";
     by (simp only: gcd_add2);
@@ -87,64 +88,65 @@
 lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)";
 proof -;
   assume "0 < n";
-  hence "gcd (n * k + m, n) = gcd (n, m mod n)"; 
+  hence "gcd (n * k + m, n) = gcd (n, m mod n)";
     by (simp add: gcd_non_0 add_commute);
   also; have "... = gcd (m, n)"; by (simp! add: gcd_non_0);
   finally; show ?thesis; .;
 qed;
 
-lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"; 
+lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)";
 proof (cases m);
   assume "m = 0";
   thus ?thesis; by simp;
 next;
-  fix k; assume "m = Suc k"; 
+  fix k; assume "m = Suc k";
   hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))";
     by (simp add: gcd_commute);
-  also; have "fib (n + k + 1) 
+  also; have "fib (n + k + 1)
     = fib (k + 1) * fib (n + 1) + fib k * fib n";
     by (rule fib_add);
-  also; have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"; 
+  also; have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))";
     by (simp add: gcd_mult_add);
-  also; have "... = gcd (fib n, fib (k + 1))"; 
+  also; have "... = gcd (fib n, fib (k + 1))";
     by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel);
-  also; have "... = gcd (fib m, fib n)"; 
+  also; have "... = gcd (fib m, fib n)";
     by (simp! add: gcd_commute);
   finally; show ?thesis; .;
 qed;
 
-lemma gcd_fib_diff: 
+lemma gcd_fib_diff:
   "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)";
-proof -; 
+proof -;
   assume "m <= n";
-  have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"; 
+  have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))";
     by (simp add: gcd_fib_add);
-  also; have "n - m + m = n"; by (simp!); 
+  also; have "n - m + m = n"; by (simp!);
   finally; show ?thesis; .;
 qed;
 
-lemma if_cases:    (* FIXME move to HOL.thy (!?) *)
-  "[| Q ==> P x; ~ Q ==> P y |] ==> P (if Q then x else y)"; by simp;
-
-lemma gcd_fib_mod: 
+lemma gcd_fib_mod:
   "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
 proof (induct n rule: less_induct);
-  fix n; 
+  fix n;
   assume m: "0 < m"
-  and hyp: "ALL ma. ma < n 
+  and hyp: "ALL ma. ma < n
            --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)";
   have "n mod m = (if n < m then n else (n - m) mod m)";
     by (rule mod_if);
   also; have "gcd (fib m, fib ...) = gcd (fib m, fib n)";
-  proof (rule if_cases);
-    assume "~ n < m"; hence m_le_n: "m <= n"; by simp;
+  proof cases;
+    assume "n < m"; thus ?thesis; by simp;
+  next;
+    assume not_lt: "~ n < m"; hence le: "m <= n"; by simp;
     have "n - m < n"; by (simp! add: diff_less);
     with hyp; have "gcd (fib m, fib ((n - m) mod m))
        = gcd (fib m, fib (n - m))"; by simp;
-    also; from m_le_n; have "... = gcd (fib m, fib n)"; 
+    also; from le; have "... = gcd (fib m, fib n)";
       by (rule gcd_fib_diff);
-    finally; show "gcd (fib m, fib ((n - m) mod m)) = gcd (fib m, fib n)"; .;
-  qed simp;
+    finally; have "gcd (fib m, fib ((n - m) mod m)) =
+      gcd (fib m, fib n)"; .;
+    with not_lt; show ?thesis; by simp;
+  qed;
   finally; show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; .;
 qed;
 

--- a/src/HOL/Isar_examples/MultisetOrder.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -25,11 +25,11 @@
 
 lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
     (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
-    (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
+    (EX K. (ALL b. b :# K --> (b, a) : r) & N = M0 + K)"
   (concl is "?case1 (mult1 r) | ?case2");
 proof (unfold mult1_def);
-  let ?r = "\\<lambda>K a. ALL b. elem K b --> (b, a) : r";
-  let ?R = "\\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
+  let ?r = "\<lambda>K a. ALL b. b :# K --> (b, a) : r";
+  let ?R = "\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
   let ?case1 = "?case1 {(N, M). ?R N M}";
 
   assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
@@ -77,7 +77,7 @@
       fix N;
       assume "(N, M0 + {#a#}) : ?R";
       hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
-          (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
+          (EX K. (ALL b. b :# K --> (b, a) : r) & N = M0 + K))";
 	by (rule less_add);
       thus "N : ?W";
       proof (elim exE disjE conjE);
@@ -88,7 +88,7 @@
       next;
 	fix K;
 	assume N: "N = M0 + K";
-	assume "ALL b. elem K b --> (b, a) : r";
+	assume "ALL b. b :# K --> (b, a) : r";
 	have "?this --> M0 + K : ?W" (is "?P K");
 	proof (induct K);
 	  from M0; have "M0 + {#} : ?W"; by simp;
@@ -97,7 +97,7 @@
 	  fix K x; assume hyp: "?P K";
 	  show "?P (K + {#x#})";
 	  proof;
-	    assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
+	    assume a: "ALL b. b :# (K + {#x#}) --> (b, a) : r";
 	    hence "(x, a) : r"; by simp;
 	    with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast;
 

--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -69,7 +69,8 @@
   by (simp add: below_def less_Suc_eq) blast;
 
 lemma Sigma_Suc2:
-    "m = n + 2 ==> A <*> below m = (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)";
+    "m = n + 2 ==> A <*> below m =
+      (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)";
   by (auto simp add: below_def) arith;
 
 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
@@ -112,7 +113,7 @@
 subsection {* Dominoes *};
 
 consts 
-  domino  :: "(nat * nat) set set";
+  domino :: "(nat * nat) set set";
 
 inductive domino
   intros

--- a/src/HOL/Isar_examples/NestedDatatype.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/NestedDatatype.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -32,7 +32,8 @@
       subst_term_list f1 (subst_term_list f2 ts)";
   by (induct t and ts rule: term.induct) simp_all;
 
-lemma "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)";
+lemma "subst_term (subst_term f1 o f2) t =
+  subst_term f1 (subst_term f2 t)";
 proof -;
   let "?P t" = ?thesis;
   let ?Q = "\\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
@@ -55,7 +56,8 @@
 subsection {* Alternative induction *};
 
 theorem term_induct' [case_names Var App]:
- "(!!a. P (Var a)) ==> (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
+  "(!!a. P (Var a)) ==>
+   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
 proof -;
   assume var: "!!a. P (Var a)";
   assume app: "!!b ts. list_all P ts ==> P (App b ts)";
@@ -76,7 +78,7 @@
 lemma
   "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
   (is "?P t");
-proof (induct ?P t rule: term_induct');
+proof (induct (open) ?P t rule: term_induct');
   case Var;
   show "?P (Var a)"; by (simp add: o_def);
 next;

--- a/src/HOL/Isar_examples/Summation.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -153,7 +153,8 @@
   show "?P 0"; by (simp add: power_eq_if);
 
   fix n;
-  have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"; by (simp add: power_eq_if distrib);
+  have "?S (n + 1) = ?S n + #4 * (n + 1)^#3";
+    by (simp add: power_eq_if distrib);
   also; assume "?S n = (n * (n + 1))^2";
   also; have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2";
     by (simp add: power_eq_if distrib);

--- a/src/HOL/Isar_examples/W_correct.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -36,8 +36,8 @@
   intros [simp]
     Var: "n < length a ==> a |- Var n :: a ! n"
     Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
-    App: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
-              ==> a |- App e1 e2 :: t1";
+    App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
+      ==> a |- App e1 e2 :: t1";
 
 
 text {* Type assigment is closed wrt.\ substitution. *};
@@ -46,7 +46,7 @@
 proof -;
   assume "a |- e :: t";
   thus ?thesis (is "?P a e t");
-  proof (induct ?P a e t);
+  proof (induct (open) ?P a e t);
     case Var;
     hence "n < length (map ($ s) a)"; by simp;
     hence "map ($ s) a |- Var n :: map ($ s) a ! n";

--- a/src/HOL/Isar_examples/document/style.tex	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/document/style.tex	Sat Aug 19 12:44:39 2000 +0200
@@ -3,6 +3,7 @@
 
 \documentclass[11pt,a4paper]{article}
 \usepackage{proof,isabelle,isabellesym,pdfsetup}
+\urlstyle{rm}
 
 \renewcommand{\isamarkupheader}[1]{\section{#1}}
 

--- a/src/HOL/Real/HahnBanach/document/root.tex	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex	Sat Aug 19 12:44:39 2000 +0200
@@ -4,6 +4,7 @@
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym,bbb}
 \usepackage{pdfsetup} %last one!
+\urlstyle{rm}
 
 \input{notation}
 
@@ -13,10 +14,8 @@
 \pagenumbering{arabic}
 
 \title{The Hahn-Banach Theorem for Real Vector Spaces}
-
 \author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
 \maketitle
-\maketitle
 
 \begin{abstract}
   The Hahn-Banach Theorem is one of the most fundamental results in functional