# HG changeset patch
# User wenzelm
# Date 999630657 -7200
# Node ID e7265e70fd7c906baf8e4a32bc643b1f69252937
# Parent  0028bd06a19cc2dbc4565641670674fe716a3359
renamed "antecedent" case to "rule_context";

diff -r 0028bd06a19c -r e7265e70fd7c NEWS
--- a/NEWS	Tue Sep 04 17:31:18 2001 +0200
+++ b/NEWS	Tue Sep 04 21:10:57 2001 +0200
@@ -5,6 +5,11 @@
 New in Isabelle2001 (?? 2001)
 -----------------------------
 
+*** Isar ***
+
+* renamed "antecedent" case to "rule_context";
+
+
 *** HOL ***
 
 * HOL: added "The" definite description operator;
diff -r 0028bd06a19c -r e7265e70fd7c doc-src/IsarRef/conversion.tex
--- a/doc-src/IsarRef/conversion.tex	Tue Sep 04 17:31:18 2001 +0200
+++ b/doc-src/IsarRef/conversion.tex	Tue Sep 04 21:10:57 2001 +0200
@@ -223,9 +223,9 @@
 Note that the above scheme repeats the text of premises $\phi@1$, \dots, while
 the conclusion $\psi$ is referenced via the automatic text abbreviation
 $\Var{thesis}$.  The assumption context may be invoked in a less verbose
-manner as well, using ``$\CASE{antecedent}$'' instead of
+manner as well, using ``$\CASE{rule_context}$'' instead of
 ``$\ASSUME{prem@1}{\phi@1}~\AND~\dots$'' above.  Then the list of \emph{all}
-premises is bound to the name $antecedent$; Isar does not provide a way to
+premises is bound to the name $rule_context$; Isar does not provide a way to
 destruct lists into single items, though.
 
 \medskip In practice, actual rules are often rather direct consequences of
diff -r 0028bd06a19c -r e7265e70fd7c doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Sep 04 17:31:18 2001 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Sep 04 21:10:57 2001 +0200
@@ -761,8 +761,8 @@
 
 Any goal statement causes some term abbreviations (such as $\Var{thesis}$,
 $\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}.
-Furthermore, the local context of a (non-atomic) goal is provided via the case
-name $antecedent$\indexisarcase{antecedent}, see also \S\ref{sec:cases}.
+Furthermore, the local context of a (non-atomic) goal is provided via the
+$rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:cases}.
 
 \medskip
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Induct/Term.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -48,11 +48,11 @@
     (!!f ts. list_all P ts ==> P (App f ts))
   ==> P t"
 proof -
-  case antecedent
+  case rule_context
   have "P t \<and> list_all P ts"
     apply (induct t and ts rule: term.induct)
-       apply (rule antecedent)
-      apply (rule antecedent)
+       apply (rule rule_context)
+      apply (rule rule_context)
       apply assumption
      apply simp_all
     done
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Lambda/ListApplication.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -108,7 +108,7 @@
     !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   |] ==> \<forall>t. size t = n --> P t"
 proof -
-  case antecedent
+  case rule_context
   show ?thesis
    apply (induct_tac n rule: nat_less_induct)
    apply (rule allI)
@@ -150,7 +150,7 @@
     !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   |] ==> P t"
 proof -
-  case antecedent
+  case rule_context
   show ?thesis
     apply (rule_tac t = t in lem)
       prefer 3
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -76,7 +76,7 @@
   ==> R"
 proof -
   assume major: "r $$ rs -> s"
-  case antecedent
+  case rule_context
   show ?thesis
     apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
     apply (assumption | rule refl | erule prems exE conjE impE disjE)+
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -331,8 +331,8 @@
   "P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1')))
     ==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
 proof -
-  case antecedent
-  note prems = this [unfolded multiset_def]
+  case rule_context
+  note premises = this [unfolded multiset_def]
   show ?thesis
     apply (unfold multiset_def)
     apply (induct_tac n)
@@ -340,7 +340,7 @@
      apply clarify
      apply (subgoal_tac "f = (\<lambda>a.0)")
       apply simp
-      apply (rule prems)
+      apply (rule premises)
      apply (rule ext)
      apply force
     apply clarify
@@ -358,7 +358,7 @@
      prefer 2
      apply (rule ext)
      apply (simp (no_asm_simp))
-     apply (erule ssubst, rule prems)
+     apply (erule ssubst, rule premises)
      apply blast
     apply (erule allE, erule impE, erule_tac [2] mp)
      apply blast
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/Quotient.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -203,7 +203,7 @@
     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
 proof -
-  case antecedent from this TrueI
+  case rule_context from this TrueI
   show ?thesis by (rule quot_cond_function)
 qed
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Library/Rational_Numbers.thy
--- a/src/HOL/Library/Rational_Numbers.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/Rational_Numbers.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -360,7 +360,7 @@
       g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==>
     f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
 proof -
-  case antecedent from this TrueI
+  case rule_context from this TrueI
   show ?thesis by (rule rat_cond_function)
 qed
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -79,14 +79,14 @@
       wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
     P s --> Q (while b c s)"
 proof -
-  case antecedent
+  case rule_context
   assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
   show ?thesis
     apply (induct s rule: wf [THEN wf_induct])
     apply simp
     apply clarify
     apply (subst while_unfold)
-    apply (simp add: antecedent)
+    apply (simp add: rule_context)
     done
 qed
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -257,7 +257,7 @@
     [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
     ==> x <=_r z \<and> y <=_r z"
     by (rule plus_le_conv [THEN iffD1])
-  case antecedent
+  case rule_context
   thus ?thesis
   apply (rule_tac iffI)
    apply clarify
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -165,7 +165,7 @@
     done
   } note this [dest]
   
-  case antecedent
+  case rule_context
   thus ?thesis by blast
 qed
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/MicroJava/BV/Product.thy
--- a/src/HOL/MicroJava/BV/Product.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/MicroJava/BV/Product.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -79,7 +79,7 @@
     "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
                  OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
     by (rule plus_le_conv [THEN iffD1])
-  case antecedent
+  case rule_context
   thus ?thesis
   apply (rule_tac iffI)
    apply clarify
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/NumberTheory/BijectionRel.thy
--- a/src/HOL/NumberTheory/BijectionRel.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -67,13 +67,13 @@
     (!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F))
   ==> P F"
 proof -
-  case antecedent
+  case rule_context
   assume major: "finite F"
     and subs: "F \<subseteq> A"
   show ?thesis
     apply (rule subs [THEN rev_mp])
     apply (rule major [THEN finite_induct])
-     apply (blast intro: antecedent)+
+     apply (blast intro: rule_context)+
     done
 qed
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/NumberTheory/EulerFermat.thy
--- a/src/HOL/NumberTheory/EulerFermat.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -71,14 +71,14 @@
       ==> P (BnorRset(a,m)) a m)
     ==> P (BnorRset(u,v)) u v"
 proof -
-  case antecedent
+  case rule_context
   show ?thesis
     apply (rule BnorRset.induct)
     apply safe
      apply (case_tac [2] "#0 < a")
-      apply (rule_tac [2] antecedent)
+      apply (rule_tac [2] rule_context)
        apply simp_all
-     apply (simp_all add: BnorRset.simps antecedent)
+     apply (simp_all add: BnorRset.simps rule_context)
   done
 qed
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/NumberTheory/IntFact.thy
--- a/src/HOL/NumberTheory/IntFact.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -58,14 +58,14 @@
       ==> P (d22set a) a)
     ==> P (d22set u) u"
 proof -
-  case antecedent
+  case rule_context
   show ?thesis
     apply (rule d22set.induct)
     apply safe
      apply (case_tac [2] "#1 < a")
-      apply (rule_tac [2] antecedent)
+      apply (rule_tac [2] rule_context)
        apply (simp_all (no_asm_simp))
-     apply (simp_all (no_asm_simp) add: d22set.simps antecedent)
+     apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
     done
 qed
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -184,14 +184,14 @@
       ==> P (wset (a, p)) a p)
     ==> P (wset (u, v)) u v"
 proof -
-  case antecedent
+  case rule_context
   show ?thesis
     apply (rule wset.induct)
     apply safe
      apply (case_tac [2] "#1 < a")
-      apply (rule_tac [2] antecedent)
+      apply (rule_tac [2] rule_context)
         apply simp_all
-      apply (simp_all add: wset.simps antecedent)
+      apply (simp_all add: wset.simps rule_context)
     done
 qed
 
diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Unix/Unix.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -618,7 +618,7 @@
   "root =xs\<Rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
     \<Longrightarrow> \<exists>att dir. root' = Env att dir"
 proof -
-  case antecedent
+  case rule_context
   with transition_type_safe show ?thesis
   proof (rule transitions_invariant)
     show "\<forall>x \<in> set xs. True" by blast
@@ -957,7 +957,7 @@
 lemma init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path"
 proof -
   note eval = "setup" access_def init_def
-  case antecedent thus ?thesis
+  case rule_context thus ?thesis
     apply (unfold bogus_def bogus_path_def)
     apply (drule transitions_consD, rule transition.intros,
       (force simp add: eval)+, (simp add: eval)?)+
@@ -1126,7 +1126,7 @@
   \<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user1) \<and>
       can_exec root (xs @ [Rmdir user1 [user1, name1]]))"
 proof -
-  case antecedent
+  case rule_context
   with cannot_rmdir init_invariant preserve_invariant
   show ?thesis by (rule general_procedure)
 qed
diff -r 0028bd06a19c -r e7265e70fd7c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 04 21:10:57 2001 +0200
@@ -580,7 +580,7 @@
 
 (* setup goals *)
 
-val antN = "antecedent";
+val rule_contextN = "rule_context";
 
 fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
   let
@@ -604,7 +604,7 @@
       commas (map (Sign.string_of_term (sign_of state)) vars));
     state'
     |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
-    |> map_context (ProofContext.add_cases (RuleCases.make true goal [antN]))
+    |> map_context (ProofContext.add_cases (RuleCases.make true goal [rule_contextN]))
     |> auto_bind_goal prop
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block