new-style definitions/abbreviations;
authorwenzelm
Thu Feb 16 21:12:00 2006 +0100 (2006-02-16)
changeset 190861b3780be6cc2
parent 19085 a1a251b297dd
child 19087 8d83af663714
new-style definitions/abbreviations;
src/HOL/Complex/ex/Sqrt.thy
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Accessible_Part.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Quotient.thy
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Complex/ex/Sqrt.thy	Thu Feb 16 21:11:58 2006 +0100
     1.2 +++ b/src/HOL/Complex/ex/Sqrt.thy	Thu Feb 16 21:12:00 2006 +0100
     1.3 @@ -17,17 +17,17 @@
     1.4    theorem.
     1.5  *}
     1.6  
     1.7 -constdefs
     1.8 -  rationals :: "real set"    ("\<rat>")
     1.9 -  "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
    1.10 +definition
    1.11 +  rationals  ("\<rat>")
    1.12 +  "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
    1.13  
    1.14 -theorem rationals_rep: "x \<in> \<rat> \<Longrightarrow>
    1.15 -  \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1"
    1.16 +theorem rationals_rep [elim?]:
    1.17 +  assumes "x \<in> \<rat>"
    1.18 +  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd (m, n) = 1"
    1.19  proof -
    1.20 -  assume "x \<in> \<rat>"
    1.21 -  then obtain m n :: nat where
    1.22 +  from `x \<in> \<rat>` obtain m n :: nat where
    1.23        n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
    1.24 -    by (unfold rationals_def) blast
    1.25 +    unfolding rationals_def by blast
    1.26    let ?gcd = "gcd (m, n)"
    1.27    from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
    1.28    let ?k = "m div ?gcd"
    1.29 @@ -58,14 +58,9 @@
    1.30      with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
    1.31      with gcd show ?thesis by simp
    1.32    qed
    1.33 -  ultimately show ?thesis by blast
    1.34 +  ultimately show ?thesis ..
    1.35  qed
    1.36  
    1.37 -lemma [elim?]: "r \<in> \<rat> \<Longrightarrow>
    1.38 -  (\<And>m n. n \<noteq> 0 \<Longrightarrow> \<bar>r\<bar> = real m / real n \<Longrightarrow> gcd (m, n) = 1 \<Longrightarrow> C)
    1.39 -    \<Longrightarrow> C"
    1.40 -  using rationals_rep by blast
    1.41 -
    1.42  
    1.43  subsection {* Main theorem *}
    1.44  
    1.45 @@ -74,10 +69,11 @@
    1.46    irrational.
    1.47  *}
    1.48  
    1.49 -theorem sqrt_prime_irrational: "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
    1.50 +theorem sqrt_prime_irrational:
    1.51 +  assumes "prime p"
    1.52 +  shows "sqrt (real p) \<notin> \<rat>"
    1.53  proof
    1.54 -  assume p_prime: "prime p"
    1.55 -  then have p: "1 < p" by (simp add: prime_def)
    1.56 +  from `prime p` have p: "1 < p" by (simp add: prime_def)
    1.57    assume "sqrt (real p) \<in> \<rat>"
    1.58    then obtain m n where
    1.59        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    1.60 @@ -94,12 +90,12 @@
    1.61    have "p dvd m \<and> p dvd n"
    1.62    proof
    1.63      from eq have "p dvd m\<twosuperior>" ..
    1.64 -    with p_prime show "p dvd m" by (rule prime_dvd_power_two)
    1.65 +    with `prime p` show "p dvd m" by (rule prime_dvd_power_two)
    1.66      then obtain k where "m = p * k" ..
    1.67      with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
    1.68      with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
    1.69      then have "p dvd n\<twosuperior>" ..
    1.70 -    with p_prime show "p dvd n" by (rule prime_dvd_power_two)
    1.71 +    with `prime p` show "p dvd n" by (rule prime_dvd_power_two)
    1.72    qed
    1.73    then have "p dvd gcd (m, n)" ..
    1.74    with gcd have "p dvd 1" by simp
    1.75 @@ -119,10 +115,11 @@
    1.76    structure, it is probably closer to proofs seen in mathematics.
    1.77  *}
    1.78  
    1.79 -theorem "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
    1.80 +theorem
    1.81 +  assumes "prime p"
    1.82 +  shows "sqrt (real p) \<notin> \<rat>"
    1.83  proof
    1.84 -  assume p_prime: "prime p"
    1.85 -  then have p: "1 < p" by (simp add: prime_def)
    1.86 +  from `prime p` have p: "1 < p" by (simp add: prime_def)
    1.87    assume "sqrt (real p) \<in> \<rat>"
    1.88    then obtain m n where
    1.89        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    1.90 @@ -134,12 +131,12 @@
    1.91    also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
    1.92    finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
    1.93    then have "p dvd m\<twosuperior>" ..
    1.94 -  with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
    1.95 +  with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
    1.96    then obtain k where "m = p * k" ..
    1.97    with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
    1.98    with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
    1.99    then have "p dvd n\<twosuperior>" ..
   1.100 -  with p_prime have "p dvd n" by (rule prime_dvd_power_two)
   1.101 +  with `prime p` have "p dvd n" by (rule prime_dvd_power_two)
   1.102    with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
   1.103    with gcd have "p dvd 1" by simp
   1.104    then have "p \<le> 1" by (simp add: dvd_imp_le)
     2.1 --- a/src/HOL/Lambda/Commutation.thy	Thu Feb 16 21:11:58 2006 +0100
     2.2 +++ b/src/HOL/Lambda/Commutation.thy	Thu Feb 16 21:12:00 2006 +0100
     2.3 @@ -10,25 +10,24 @@
     2.4  
     2.5  subsection {* Basic definitions *}
     2.6  
     2.7 -constdefs
     2.8 +definition
     2.9    square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
    2.10 -  "square R S T U ==
    2.11 -    \<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U))"
    2.12 +  "square R S T U =
    2.13 +    (\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U)))"
    2.14  
    2.15    commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
    2.16 -  "commute R S == square R S S R"
    2.17 +  "commute R S = square R S S R"
    2.18  
    2.19    diamond :: "('a \<times> 'a) set => bool"
    2.20 -  "diamond R == commute R R"
    2.21 +  "diamond R = commute R R"
    2.22  
    2.23    Church_Rosser :: "('a \<times> 'a) set => bool"
    2.24 -  "Church_Rosser R ==
    2.25 -    \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
    2.26 +  "Church_Rosser R =
    2.27 +    (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
    2.28  
    2.29 -syntax
    2.30 +abbreviation (output)
    2.31    confluent :: "('a \<times> 'a) set => bool"
    2.32 -translations
    2.33 -  "confluent R" == "diamond (R^*)"
    2.34 +  "confluent R = diamond (R^*)"
    2.35  
    2.36  
    2.37  subsection {* Basic lemmas *}
     3.1 --- a/src/HOL/Lambda/Eta.thy	Thu Feb 16 21:11:58 2006 +0100
     3.2 +++ b/src/HOL/Lambda/Eta.thy	Thu Feb 16 21:12:00 2006 +0100
     3.3 @@ -21,14 +21,13 @@
     3.4  consts
     3.5    eta :: "(dB \<times> dB) set"
     3.6  
     3.7 -syntax 
     3.8 -  "_eta" :: "[dB, dB] => bool"   (infixl "-e>" 50)
     3.9 -  "_eta_rtrancl" :: "[dB, dB] => bool"   (infixl "-e>>" 50)
    3.10 -  "_eta_reflcl" :: "[dB, dB] => bool"   (infixl "-e>=" 50)
    3.11 -translations
    3.12 -  "s -e> t" == "(s, t) \<in> eta"
    3.13 -  "s -e>> t" == "(s, t) \<in> eta^*"
    3.14 -  "s -e>= t" == "(s, t) \<in> eta^="
    3.15 +abbreviation (output)
    3.16 +  eta_red :: "[dB, dB] => bool"   (infixl "-e>" 50)
    3.17 +  "(s -e> t) = ((s, t) \<in> eta)"
    3.18 +  eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50)
    3.19 +  "(s -e>> t) = ((s, t) \<in> eta^*)"
    3.20 +  eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50)
    3.21 +  "(s -e>= t) = ((s, t) \<in> eta^=)"
    3.22  
    3.23  inductive eta
    3.24    intros
    3.25 @@ -225,13 +224,12 @@
    3.26  consts
    3.27    par_eta :: "(dB \<times> dB) set"
    3.28  
    3.29 -syntax 
    3.30 -  "_par_eta" :: "[dB, dB] => bool"   (infixl "=e>" 50)
    3.31 -translations
    3.32 -  "s =e> t" == "(s, t) \<in> par_eta"
    3.33 +abbreviation (output)
    3.34 +  par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
    3.35 +  "(s =e> t) = ((s, t) \<in> par_eta)"
    3.36  
    3.37  syntax (xsymbols)
    3.38 -  "_par_eta" :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
    3.39 +  par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
    3.40  
    3.41  inductive par_eta
    3.42  intros
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Thu Feb 16 21:11:58 2006 +0100
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Thu Feb 16 21:12:00 2006 +0100
     4.3 @@ -56,15 +56,15 @@
     4.4  consts
     4.5    beta :: "(dB \<times> dB) set"
     4.6  
     4.7 -syntax
     4.8 -  "_beta" :: "[dB, dB] => bool"  (infixl "->" 50)
     4.9 -  "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->>" 50)
    4.10 +abbreviation (output)
    4.11 +  beta_red :: "[dB, dB] => bool"  (infixl "->" 50)
    4.12 +  "(s -> t) = ((s, t) \<in> beta)"
    4.13 +  beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
    4.14 +  "(s ->> t) = ((s, t) \<in> beta^*)"
    4.15 +
    4.16  syntax (latex)
    4.17 -  "_beta" :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
    4.18 -  "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    4.19 -translations
    4.20 -  "s \<rightarrow>\<^sub>\<beta> t" == "(s, t) \<in> beta"
    4.21 -  "s \<rightarrow>\<^sub>\<beta>\<^sup>* t" == "(s, t) \<in> beta^*"
    4.22 +  beta_red :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
    4.23 +  beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    4.24  
    4.25  inductive beta
    4.26    intros
     5.1 --- a/src/HOL/Lambda/ListApplication.thy	Thu Feb 16 21:11:58 2006 +0100
     5.2 +++ b/src/HOL/Lambda/ListApplication.thy	Thu Feb 16 21:12:00 2006 +0100
     5.3 @@ -8,10 +8,9 @@
     5.4  
     5.5  theory ListApplication imports Lambda begin
     5.6  
     5.7 -syntax
     5.8 -  "_list_application" :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
     5.9 -translations
    5.10 -  "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
    5.11 +abbreviation (output)
    5.12 +  list_application :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
    5.13 +  "t \<degree>\<degree> ts = foldl (op \<degree>) t ts"
    5.14  
    5.15  lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
    5.16    by (induct ts rule: rev_induct) auto
     6.1 --- a/src/HOL/Lambda/ListBeta.thy	Thu Feb 16 21:11:58 2006 +0100
     6.2 +++ b/src/HOL/Lambda/ListBeta.thy	Thu Feb 16 21:12:00 2006 +0100
     6.3 @@ -12,10 +12,9 @@
     6.4    Lifting beta-reduction to lists of terms, reducing exactly one element.
     6.5  *}
     6.6  
     6.7 -syntax
     6.8 -  "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
     6.9 -translations
    6.10 -  "rs => ss" == "(rs, ss) : step1 beta"
    6.11 +abbreviation (output)
    6.12 +  list_beta :: "dB list => dB list => bool"   (infixl "=>" 50)
    6.13 +  "(rs => ss) = ((rs, ss) : step1 beta)"
    6.14  
    6.15  lemma head_Var_reduction:
    6.16    "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
     7.1 --- a/src/HOL/Lambda/ListOrder.thy	Thu Feb 16 21:11:58 2006 +0100
     7.2 +++ b/src/HOL/Lambda/ListOrder.thy	Thu Feb 16 21:12:00 2006 +0100
     7.3 @@ -13,9 +13,9 @@
     7.4    element.
     7.5  *}
     7.6  
     7.7 -constdefs
     7.8 +definition
     7.9    step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
    7.10 -  "step1 r ==
    7.11 +  "step1 r =
    7.12      {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
    7.13        us @ z' # vs}"
    7.14  
     8.1 --- a/src/HOL/Lambda/ParRed.thy	Thu Feb 16 21:11:58 2006 +0100
     8.2 +++ b/src/HOL/Lambda/ParRed.thy	Thu Feb 16 21:12:00 2006 +0100
     8.3 @@ -17,10 +17,9 @@
     8.4  consts
     8.5    par_beta :: "(dB \<times> dB) set"
     8.6  
     8.7 -syntax
     8.8 -  par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
     8.9 -translations
    8.10 -  "s => t" == "(s, t) \<in> par_beta"
    8.11 +abbreviation (output)
    8.12 +  par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50)
    8.13 +  "(s => t) = ((s, t) \<in> par_beta)"
    8.14  
    8.15  inductive par_beta
    8.16    intros
     9.1 --- a/src/HOL/Lambda/Type.thy	Thu Feb 16 21:11:58 2006 +0100
     9.2 +++ b/src/HOL/Lambda/Type.thy	Thu Feb 16 21:12:00 2006 +0100
     9.3 @@ -11,9 +11,9 @@
     9.4  
     9.5  subsection {* Environments *}
     9.6  
     9.7 -constdefs
     9.8 +definition
     9.9    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
    9.10 -  "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
    9.11 +  "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
    9.12  syntax (xsymbols)
    9.13    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    9.14  syntax (HTML output)
    9.15 @@ -47,21 +47,23 @@
    9.16    typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
    9.17    typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    9.18  
    9.19 -syntax
    9.20 -  "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
    9.21 -  "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
    9.22 -  "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    9.23 +abbreviation (output)
    9.24 +  funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
    9.25 +  "Ts =>> T = foldr Fun Ts T"
    9.26 +
    9.27 +  typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
    9.28 +  "(env |- t : T) = ((env, t, T) \<in> typing)"
    9.29 +
    9.30 +  typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    9.31      ("_ ||- _ : _" [50, 50, 50] 50)
    9.32 +  "(env ||- ts : Ts) = typings env ts Ts"
    9.33 +
    9.34  syntax (xsymbols)
    9.35 -  "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    9.36 +  typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    9.37  syntax (latex)
    9.38 -  "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
    9.39 -  "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    9.40 +  funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
    9.41 +  typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    9.42      ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
    9.43 -translations
    9.44 -  "Ts \<Rrightarrow> T" \<rightleftharpoons> "foldr Fun Ts T"
    9.45 -  "env \<turnstile> t : T" \<rightleftharpoons> "(env, t, T) \<in> typing"
    9.46 -  "env \<tturnstile> ts : Ts" \<rightleftharpoons> "typings env ts Ts"
    9.47  
    9.48  inductive typing
    9.49    intros
    10.1 --- a/src/HOL/Lambda/WeakNorm.thy	Thu Feb 16 21:11:58 2006 +0100
    10.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Thu Feb 16 21:12:00 2006 +0100
    10.3 @@ -16,9 +16,9 @@
    10.4  
    10.5  subsection {* Terms in normal form *}
    10.6  
    10.7 -constdefs
    10.8 +definition
    10.9    listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
   10.10 -  "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
   10.11 +  "listall P xs == (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
   10.12  
   10.13  declare listall_def [extraction_expand]
   10.14  
   10.15 @@ -361,12 +361,11 @@
   10.16  consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
   10.17    rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
   10.18  
   10.19 -syntax
   10.20 -  "_rtyping" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
   10.21 +abbreviation (output)
   10.22 +  rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
   10.23 +  "(e |-\<^sub>R t : T) = ((e, t, T) \<in> rtyping)"
   10.24  syntax (xsymbols)
   10.25 -  "_rtyping" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   10.26 -translations
   10.27 -  "e \<turnstile>\<^sub>R t : T" \<rightleftharpoons> "(e, t, T) \<in> rtyping"
   10.28 +  rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   10.29  
   10.30  inductive rtyping
   10.31    intros
    11.1 --- a/src/HOL/Library/Accessible_Part.thy	Thu Feb 16 21:11:58 2006 +0100
    11.2 +++ b/src/HOL/Library/Accessible_Part.thy	Thu Feb 16 21:12:00 2006 +0100
    11.3 @@ -23,10 +23,9 @@
    11.4    intros
    11.5      accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
    11.6  
    11.7 -syntax
    11.8 +abbreviation (output)
    11.9    termi :: "('a \<times> 'a) set => 'a set"
   11.10 -translations
   11.11 -  "termi r" == "acc (r\<inverse>)"
   11.12 +  "termi r == acc (r\<inverse>)"
   11.13  
   11.14  
   11.15  subsection {* Induction rules *}
    12.1 --- a/src/HOL/Library/Coinductive_List.thy	Thu Feb 16 21:11:58 2006 +0100
    12.2 +++ b/src/HOL/Library/Coinductive_List.thy	Thu Feb 16 21:12:00 2006 +0100
    12.3 @@ -11,12 +11,9 @@
    12.4  
    12.5  subsection {* List constructors over the datatype universe *}
    12.6  
    12.7 -constdefs
    12.8 -  NIL :: "'a Datatype_Universe.item"
    12.9 -  "NIL \<equiv> Datatype_Universe.In0 (Datatype_Universe.Numb 0)"
   12.10 -  CONS :: "'a Datatype_Universe.item \<Rightarrow> 'a Datatype_Universe.item
   12.11 -    \<Rightarrow> 'a Datatype_Universe.item"
   12.12 -  "CONS M N \<equiv> Datatype_Universe.In1 (Datatype_Universe.Scons M N)"
   12.13 +definition
   12.14 +  "NIL = Datatype_Universe.In0 (Datatype_Universe.Numb 0)"
   12.15 +  "CONS M N = Datatype_Universe.In1 (Datatype_Universe.Scons M N)"
   12.16  
   12.17  lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL"
   12.18    and NIL_not_CONS [iff]: "NIL \<noteq> CONS M N"
   12.19 @@ -30,9 +27,8 @@
   12.20      -- {* A continuity result? *}
   12.21    by (simp add: CONS_def In1_UN1 Scons_UN1_y)
   12.22  
   12.23 -constdefs
   12.24 -  List_case where
   12.25 -  "List_case c h \<equiv> Datatype_Universe.Case (\<lambda>_. c) (Datatype_Universe.Split h)"
   12.26 +definition
   12.27 +  "List_case c h = Datatype_Universe.Case (\<lambda>_. c) (Datatype_Universe.Split h)"
   12.28  
   12.29  lemma List_case_NIL [simp]: "List_case c h NIL = c"
   12.30    and List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
   12.31 @@ -63,10 +59,8 @@
   12.32        None \<Rightarrow> NIL
   12.33      | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
   12.34  
   12.35 -constdefs
   12.36 -  LList_corec :: "'a \<Rightarrow> ('a \<Rightarrow> ('b Datatype_Universe.item \<times> 'a) option) \<Rightarrow>
   12.37 -    'b Datatype_Universe.item"
   12.38 -  "LList_corec a f \<equiv> \<Union>k. LList_corec_aux k f a"
   12.39 +definition
   12.40 +  "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
   12.41  
   12.42  text {*
   12.43    Note: the subsequent recursion equation for @{text LList_corec} may
   12.44 @@ -150,12 +144,9 @@
   12.45    finally show ?thesis .
   12.46  qed
   12.47  
   12.48 -constdefs
   12.49 -  LNil :: "'a llist"
   12.50 -  "LNil \<equiv> Abs_llist NIL"
   12.51 -
   12.52 -  LCons :: "'a \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
   12.53 -  "LCons x xs \<equiv> Abs_llist (CONS (Datatype_Universe.Leaf x) (Rep_llist xs))"
   12.54 +definition
   12.55 +  "LNil = Abs_llist NIL"
   12.56 +  "LCons x xs = Abs_llist (CONS (Datatype_Universe.Leaf x) (Rep_llist xs))"
   12.57  
   12.58  lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
   12.59    apply (simp add: LNil_def LCons_def)
   12.60 @@ -202,11 +193,9 @@
   12.61  qed
   12.62  
   12.63  
   12.64 -constdefs
   12.65 -  llist_case :: "'b \<Rightarrow> ('a \<Rightarrow> 'a llist \<Rightarrow> 'b) \<Rightarrow> 'a llist \<Rightarrow> 'b"
   12.66 -  "llist_case c d l \<equiv>
   12.67 +definition
   12.68 +  "llist_case c d l =
   12.69      List_case c (\<lambda>x y. d (inv Datatype_Universe.Leaf x) (Abs_llist y)) (Rep_llist l)"
   12.70 -
   12.71  translations
   12.72    "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "llist_case a (\<lambda>x l. b) p"
   12.73  
   12.74 @@ -219,9 +208,8 @@
   12.75      CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
   12.76  
   12.77  
   12.78 -constdefs
   12.79 -  llist_corec :: "'a \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> 'b llist"
   12.80 -  "llist_corec a f \<equiv>
   12.81 +definition
   12.82 +  "llist_corec a f =
   12.83      Abs_llist (LList_corec a
   12.84        (\<lambda>z.
   12.85          case f z of None \<Rightarrow> None
   12.86 @@ -539,8 +527,7 @@
   12.87  
   12.88  subsubsection {* @{text Lconst} *}
   12.89  
   12.90 -constdefs
   12.91 -  Lconst where
   12.92 +definition
   12.93    "Lconst M \<equiv> lfp (\<lambda>N. CONS M N)"
   12.94  
   12.95  lemma Lconst_fun_mono: "mono (CONS M)"
   12.96 @@ -580,12 +567,9 @@
   12.97  
   12.98  subsubsection {* @{text Lmap} and @{text lmap} *}
   12.99  
  12.100 -constdefs
  12.101 -  Lmap where
  12.102 -  "Lmap f M \<equiv> LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
  12.103 -
  12.104 -  lmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a llist \<Rightarrow> 'b llist"
  12.105 -  "lmap f l \<equiv> llist_corec l
  12.106 +definition
  12.107 +  "Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
  12.108 +  "lmap f l = llist_corec l
  12.109      (\<lambda>z.
  12.110        case z of LNil \<Rightarrow> None
  12.111        | LCons y z \<Rightarrow> Some (f y, z))"
  12.112 @@ -678,15 +662,12 @@
  12.113  
  12.114  subsubsection {* @{text Lappend} *}
  12.115  
  12.116 -constdefs
  12.117 -  Lappend where
  12.118 -  "Lappend M N \<equiv> LList_corec (M, N)
  12.119 +definition
  12.120 +  "Lappend M N = LList_corec (M, N)
  12.121      (split (List_case
  12.122          (List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2))))
  12.123          (\<lambda>M1 M2 N. Some (M1, (M2, N)))))"
  12.124 -
  12.125 -  lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
  12.126 -  "lappend l n \<equiv> llist_corec (l, n)
  12.127 +  "lappend l n = llist_corec (l, n)
  12.128      (split (llist_case
  12.129          (llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2))))
  12.130          (\<lambda>l1 l2 n. Some (l1, (l2, n)))))"
  12.131 @@ -760,9 +741,9 @@
  12.132  
  12.133  text {* @{text llist_fun_equalityI} cannot be used here! *}
  12.134  
  12.135 -constdefs
  12.136 +definition
  12.137    iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
  12.138 -  "iterates f a \<equiv> llist_corec a (\<lambda>x. Some (x, f x))"
  12.139 +  "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
  12.140  
  12.141  lemma iterates: "iterates f x = LCons x (iterates f (f x))"
  12.142    apply (unfold iterates_def)
    13.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Feb 16 21:11:58 2006 +0100
    13.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Feb 16 21:12:00 2006 +0100
    13.3 @@ -155,9 +155,9 @@
    13.4  
    13.5  subsection {* Parallel lists *}
    13.6  
    13.7 -constdefs
    13.8 +definition
    13.9    parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
   13.10 -  "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
   13.11 +  "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
   13.12  
   13.13  lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
   13.14    unfolding parallel_def by blast
   13.15 @@ -215,9 +215,9 @@
   13.16  
   13.17  subsection {* Postfix order on lists *}
   13.18  
   13.19 -constdefs
   13.20 +definition
   13.21    postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50)
   13.22 -  "xs >>= ys == \<exists>zs. xs = zs @ ys"
   13.23 +  "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"
   13.24  
   13.25  lemma postfix_refl [simp, intro!]: "xs >>= xs"
   13.26    by (auto simp add: postfix_def)
    14.1 --- a/src/HOL/Library/Multiset.thy	Thu Feb 16 21:11:58 2006 +0100
    14.2 +++ b/src/HOL/Library/Multiset.thy	Thu Feb 16 21:12:00 2006 +0100
    14.3 @@ -20,29 +20,31 @@
    14.4      Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
    14.5    and [simp] = Rep_multiset_inject [symmetric]
    14.6  
    14.7 -constdefs
    14.8 +definition
    14.9    Mempty :: "'a multiset"    ("{#}")
   14.10 -  "{#} == Abs_multiset (\<lambda>a. 0)"
   14.11 +  "{#} = Abs_multiset (\<lambda>a. 0)"
   14.12  
   14.13    single :: "'a => 'a multiset"    ("{#_#}")
   14.14 -  "{#a#} == Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
   14.15 +  "{#a#} = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
   14.16  
   14.17    count :: "'a multiset => 'a => nat"
   14.18 -  "count == Rep_multiset"
   14.19 +  "count = Rep_multiset"
   14.20  
   14.21    MCollect :: "'a multiset => ('a => bool) => 'a multiset"
   14.22 -  "MCollect M P == Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
   14.23 +  "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
   14.24 +
   14.25 +abbreviation (output)
   14.26 +  Melem :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
   14.27 +  "(a :# M) = (0 < count M a)"
   14.28  
   14.29  syntax
   14.30 -  "_Melem" :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
   14.31    "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
   14.32  translations
   14.33 -  "a :# M" == "0 < count M a"
   14.34    "{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
   14.35  
   14.36 -constdefs
   14.37 +definition
   14.38    set_of :: "'a multiset => 'a set"
   14.39 -  "set_of M == {x. x :# M}"
   14.40 +  "set_of M = {x. x :# M}"
   14.41  
   14.42  instance multiset :: (type) "{plus, minus, zero}" ..
   14.43  
   14.44 @@ -52,9 +54,9 @@
   14.45    Zero_multiset_def [simp]: "0 == {#}"
   14.46    size_def: "size M == setsum (count M) (set_of M)"
   14.47  
   14.48 -constdefs
   14.49 - multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
   14.50 - "multiset_inter A B \<equiv> A - (A - B)"
   14.51 +definition
   14.52 +  multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
   14.53 +  "multiset_inter A B = A - (A - B)"
   14.54  
   14.55  
   14.56  text {*
   14.57 @@ -377,14 +379,14 @@
   14.58  
   14.59  subsubsection {* Well-foundedness *}
   14.60  
   14.61 -constdefs
   14.62 +definition
   14.63    mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
   14.64 -  "mult1 r ==
   14.65 +  "mult1 r =
   14.66      {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
   14.67        (\<forall>b. b :# K --> (b, a) \<in> r)}"
   14.68  
   14.69    mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
   14.70 -  "mult r == (mult1 r)\<^sup>+"
   14.71 +  "mult r = (mult1 r)\<^sup>+"
   14.72  
   14.73  lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   14.74    by (simp add: mult1_def)
   14.75 @@ -793,16 +795,9 @@
   14.76  
   14.77  subsection {* Pointwise ordering induced by count *}
   14.78  
   14.79 -consts
   14.80 -  mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"
   14.81 -
   14.82 -syntax
   14.83 -  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50)
   14.84 -translations
   14.85 -  "x \<le># y" == "mset_le x y"
   14.86 -
   14.87 -defs
   14.88 -  mset_le_def: "xs \<le># ys == (\<forall>a. count xs a \<le> count ys a)"
   14.89 +definition
   14.90 +  mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50)
   14.91 +  "(xs \<le># ys) = (\<forall>a. count xs a \<le> count ys a)"
   14.92  
   14.93  lemma mset_le_refl[simp]: "xs \<le># xs"
   14.94    unfolding mset_le_def by auto
    15.1 --- a/src/HOL/Library/Primes.thy	Thu Feb 16 21:11:58 2006 +0100
    15.2 +++ b/src/HOL/Library/Primes.thy	Thu Feb 16 21:12:00 2006 +0100
    15.3 @@ -10,12 +10,12 @@
    15.4  imports Main
    15.5  begin
    15.6  
    15.7 -constdefs
    15.8 +definition
    15.9    coprime :: "nat => nat => bool"
   15.10 -  "coprime m n == gcd (m, n) = 1"
   15.11 +  "coprime m n = (gcd (m, n) = 1)"
   15.12  
   15.13    prime :: "nat \<Rightarrow> bool"
   15.14 -  "prime p == 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)"
   15.15 +  "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
   15.16  
   15.17  
   15.18  lemma two_is_prime: "prime 2"
    16.1 --- a/src/HOL/Library/Quotient.thy	Thu Feb 16 21:11:58 2006 +0100
    16.2 +++ b/src/HOL/Library/Quotient.thy	Thu Feb 16 21:12:00 2006 +0100
    16.3 @@ -74,9 +74,9 @@
    16.4   representation of elements of a quotient type.
    16.5  *}
    16.6  
    16.7 -constdefs
    16.8 +definition
    16.9    "class" :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
   16.10 -  "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
   16.11 +  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
   16.12  
   16.13  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
   16.14  proof (cases A)
   16.15 @@ -133,9 +133,9 @@
   16.16  
   16.17  subsection {* Picking representing elements *}
   16.18  
   16.19 -constdefs
   16.20 +definition
   16.21    pick :: "'a::equiv quot => 'a"
   16.22 -  "pick A == SOME a. A = \<lfloor>a\<rfloor>"
   16.23 +  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
   16.24  
   16.25  theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
   16.26  proof (unfold pick_def)
    17.1 --- a/src/HOL/Unix/Unix.thy	Thu Feb 16 21:11:58 2006 +0100
    17.2 +++ b/src/HOL/Unix/Unix.thy	Thu Feb 16 21:12:00 2006 +0100
    17.3 @@ -160,15 +160,13 @@
    17.4    \cite{Nipkow-et-al:2000:HOL}.
    17.5  *}
    17.6  
    17.7 -constdefs
    17.8 -  attributes :: "file \<Rightarrow> att"
    17.9 -  "attributes file \<equiv>
   17.10 +definition
   17.11 +  "attributes file =
   17.12      (case file of
   17.13        Val (att, text) \<Rightarrow> att
   17.14      | Env att dir \<Rightarrow> att)"
   17.15  
   17.16 -  attributes_update :: "att \<Rightarrow> file \<Rightarrow> file"
   17.17 -  "attributes_update att file \<equiv>
   17.18 +  "attributes_update att file =
   17.19      (case file of
   17.20        Val (att', text) \<Rightarrow> Val (att, text)
   17.21      | Env att' dir \<Rightarrow> Env att dir)"
   17.22 @@ -201,9 +199,8 @@
   17.23    has user id 0).
   17.24  *}
   17.25  
   17.26 -constdefs
   17.27 -  init :: "uid set \<Rightarrow> file"
   17.28 -  "init users \<equiv>
   17.29 +definition
   17.30 +  "init users =
   17.31      Env \<lparr>owner = 0, others = {Readable}\<rparr>
   17.32        (\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty)
   17.33          else None)"
   17.34 @@ -223,8 +220,7 @@
   17.35    access a file unconditionally (in our simplified model).
   17.36  *}
   17.37  
   17.38 -constdefs
   17.39 -  access :: "file \<Rightarrow> path \<Rightarrow> uid \<Rightarrow> perms \<Rightarrow> file option"
   17.40 +definition
   17.41    "access root path uid perms \<equiv>
   17.42      (case lookup root path of
   17.43        None \<Rightarrow> None
   17.44 @@ -648,8 +644,7 @@
   17.45    transition.
   17.46  *}
   17.47  
   17.48 -constdefs
   17.49 -  can_exec :: "file \<Rightarrow> operation list \<Rightarrow> bool"
   17.50 +definition
   17.51    "can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'"
   17.52  
   17.53  lemma can_exec_nil: "can_exec root []"
   17.54 @@ -843,13 +838,12 @@
   17.55    notes facts = user\<^isub>1_known user\<^isub>1_not_root users_neq
   17.56      perms\<^isub>1_writable perms\<^isub>2_not_writable
   17.57  
   17.58 -  fixes bogus :: "operation list"
   17.59 -    and bogus_path :: path
   17.60 -  defines "bogus \<equiv>
   17.61 +definition (in situation)
   17.62 +  "bogus =
   17.63       [Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],
   17.64        Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],
   17.65        Creat user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
   17.66 -    and "bogus_path \<equiv> [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
   17.67 +  "bogus_path = [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
   17.68  
   17.69  text {*
   17.70    The @{term bogus} operations are the ones that lead into the uncouth
   17.71 @@ -867,9 +861,8 @@
   17.72    neither owned and nor writable by @{term user\<^isub>1}.
   17.73  *}
   17.74  
   17.75 -locale invariant = situation +
   17.76 -  fixes invariant :: "file \<Rightarrow> path \<Rightarrow> bool"
   17.77 -  defines "invariant root path \<equiv>
   17.78 +definition (in situation)
   17.79 +  "invariant root path \<equiv>
   17.80      (\<exists>att dir.
   17.81        access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
   17.82        user\<^isub>1 \<noteq> owner att \<and>
   17.83 @@ -907,7 +900,7 @@
   17.84    we just have to inspect rather special cases.
   17.85  *}
   17.86  
   17.87 -lemma (in invariant) cannot_rmdir:
   17.88 +lemma (in situation) cannot_rmdir:
   17.89    assumes inv: "invariant root bogus_path"
   17.90      and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
   17.91    shows False
   17.92 @@ -923,7 +916,7 @@
   17.93    ultimately show False by (simp add: bogus_path_def)
   17.94  qed
   17.95  
   17.96 -lemma (in invariant)
   17.97 +lemma (in situation)
   17.98    assumes init: "init users =bogus\<Rightarrow> root"
   17.99    notes eval = facts access_def init_def
  17.100    shows init_invariant: "invariant root bogus_path"
  17.101 @@ -946,7 +939,7 @@
  17.102    required here.
  17.103  *}
  17.104  
  17.105 -lemma (in invariant) preserve_invariant:
  17.106 +lemma (in situation) preserve_invariant:
  17.107    assumes tr: "root \<midarrow>x\<rightarrow> root'"
  17.108      and inv: "invariant root path"
  17.109      and uid: "uid_of x = user\<^isub>1"
  17.110 @@ -1090,8 +1083,7 @@
  17.111    overall procedure (see \secref{sec:unix-inv-procedure}).
  17.112  *}
  17.113  
  17.114 -corollary result:
  17.115 -  includes invariant
  17.116 +corollary (in situation)
  17.117    assumes bogus: "init users =bogus\<Rightarrow> root"
  17.118    shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and>
  17.119      can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))"
  17.120 @@ -1100,11 +1092,4 @@
  17.121      and bogus show ?thesis by (rule general_procedure)
  17.122  qed
  17.123  
  17.124 -text {*
  17.125 -  So this is our final result:
  17.126 -
  17.127 -  @{thm [display, show_question_marks = false] result [OF
  17.128 -  invariant.intro, OF situation.intro]}
  17.129 -*}
  17.130 -
  17.131  end