merged
authorAndreas Lochbihler
Wed Oct 10 16:41:19 2012 +0200 (2012-10-10)
changeset 498113fc6b3289c31
parent 49810 53f14f62cca2
parent 49806 acb6fa98e310
child 49812 e3945ddcb9aa
merged
     1.1 --- a/src/Cube/Cube.thy	Wed Oct 10 16:18:27 2012 +0200
     1.2 +++ b/src/Cube/Cube.thy	Wed Oct 10 16:41:19 2012 +0200
     1.3 @@ -10,6 +10,15 @@
     1.4  
     1.5  setup Pure_Thy.old_appl_syntax_setup
     1.6  
     1.7 +ML {*
     1.8 +  structure Rules = Named_Thms
     1.9 +  (
    1.10 +    val name = @{binding rules}
    1.11 +    val description = "Cube inference rules"
    1.12 +  )
    1.13 +*}
    1.14 +setup Rules.setup
    1.15 +
    1.16  typedecl "term"
    1.17  typedecl "context"
    1.18  typedecl typing
    1.19 @@ -72,8 +81,7 @@
    1.20  
    1.21    beta: "Abs(A, f)^a == f(a)"
    1.22  
    1.23 -lemmas simple = s_b strip_s strip_b app lam_ss pi_ss
    1.24 -lemmas rules = simple
    1.25 +lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
    1.26  
    1.27  lemma imp_elim:
    1.28    assumes "f:A\<rightarrow>B" and "a:A" and "f^a:B ==> PROP P"
    1.29 @@ -90,7 +98,7 @@
    1.30                     ==> Abs(A,f) : Prod(A,B)"
    1.31  begin
    1.32  
    1.33 -lemmas rules = simple lam_bs pi_bs
    1.34 +lemmas [rules] = lam_bs pi_bs
    1.35  
    1.36  end
    1.37  
    1.38 @@ -102,7 +110,7 @@
    1.39                     ==> Abs(A,f) : Prod(A,B)"
    1.40  begin
    1.41  
    1.42 -lemmas rules = simple lam_bb pi_bb
    1.43 +lemmas [rules] = lam_bb pi_bb
    1.44  
    1.45  end
    1.46  
    1.47 @@ -113,7 +121,7 @@
    1.48                     ==> Abs(A,f) : Prod(A,B)"
    1.49  begin
    1.50  
    1.51 -lemmas rules = simple lam_sb pi_sb
    1.52 +lemmas [rules] = lam_sb pi_sb
    1.53  
    1.54  end
    1.55  
    1.56 @@ -121,7 +129,7 @@
    1.57  locale LP2 = LP + L2
    1.58  begin
    1.59  
    1.60 -lemmas rules = simple lam_bs pi_bs lam_sb pi_sb
    1.61 +lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
    1.62  
    1.63  end
    1.64  
    1.65 @@ -129,7 +137,7 @@
    1.66  locale Lomega2 = L2 + Lomega
    1.67  begin
    1.68  
    1.69 -lemmas rules = simple lam_bs pi_bs lam_bb pi_bb
    1.70 +lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
    1.71  
    1.72  end
    1.73  
    1.74 @@ -137,7 +145,7 @@
    1.75  locale LPomega = LP + Lomega
    1.76  begin
    1.77  
    1.78 -lemmas rules = simple lam_bb pi_bb lam_sb pi_sb
    1.79 +lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
    1.80  
    1.81  end
    1.82  
    1.83 @@ -145,7 +153,7 @@
    1.84  locale CC = L2 + LP + Lomega
    1.85  begin
    1.86  
    1.87 -lemmas rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
    1.88 +lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
    1.89  
    1.90  end
    1.91  
     2.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Oct 10 16:18:27 2012 +0200
     2.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Oct 10 16:41:19 2012 +0200
     2.3 @@ -104,7 +104,7 @@
     2.4  end
     2.5  print_locale! logic
     2.6  
     2.7 -locale use_decl = logic + semi "op ||"
     2.8 +locale use_decl = l: logic + semi "op ||"
     2.9  print_locale! use_decl thm use_decl_def
    2.10  
    2.11  locale extra_type =
     3.1 --- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Wed Oct 10 16:18:27 2012 +0200
     3.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Wed Oct 10 16:41:19 2012 +0200
     3.3 @@ -273,7 +273,7 @@
     3.4  
     3.5  
     3.6  lemma embed_underS:
     3.7 -assumes WELL: "Well_order r" and WELL: "Well_order r'" and
     3.8 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
     3.9          EMB: "embed r r' f" and IN: "a \<in> Field r"
    3.10  shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
    3.11  proof-
     4.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Oct 10 16:18:27 2012 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Oct 10 16:41:19 2012 +0200
     4.3 @@ -452,7 +452,7 @@
     4.4    assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
     4.5      and between_same: "between x x = x"
     4.6  
     4.7 -sublocale  constr_dense_linorder < dense_linorder 
     4.8 +sublocale  constr_dense_linorder < dlo: dense_linorder 
     4.9    apply unfold_locales
    4.10    using gt_ex lt_ex between_less
    4.11    apply auto
     5.1 --- a/src/HOL/Finite_Set.thy	Wed Oct 10 16:18:27 2012 +0200
     5.2 +++ b/src/HOL/Finite_Set.thy	Wed Oct 10 16:41:19 2012 +0200
     5.3 @@ -1757,7 +1757,7 @@
     5.4  locale folding_image_simple_idem = folding_image_simple +
     5.5    assumes idem: "x * x = x"
     5.6  
     5.7 -sublocale folding_image_simple_idem < semilattice proof
     5.8 +sublocale folding_image_simple_idem < semilattice: semilattice proof
     5.9  qed (fact idem)
    5.10  
    5.11  context folding_image_simple_idem
    5.12 @@ -1898,7 +1898,7 @@
    5.13  locale folding_one_idem = folding_one +
    5.14    assumes idem: "x * x = x"
    5.15  
    5.16 -sublocale folding_one_idem < semilattice proof
    5.17 +sublocale folding_one_idem < semilattice: semilattice proof
    5.18  qed (fact idem)
    5.19  
    5.20  context folding_one_idem
     6.1 --- a/src/HOL/Library/Univ_Poly.thy	Wed Oct 10 16:18:27 2012 +0200
     6.2 +++ b/src/HOL/Library/Univ_Poly.thy	Wed Oct 10 16:41:19 2012 +0200
     6.3 @@ -414,7 +414,6 @@
     6.4  apply (auto simp add: poly_exp poly_mult)
     6.5  done
     6.6  
     6.7 -lemma (in semiring_1) one_neq_zero[simp]: "1 \<noteq> 0" using zero_neq_one by blast
     6.8  lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \<noteq> poly []"
     6.9  apply (simp add: fun_eq)
    6.10  apply (rule_tac x = "minus one a" in exI)
     7.1 --- a/src/HOL/NthRoot.thy	Wed Oct 10 16:18:27 2012 +0200
     7.2 +++ b/src/HOL/NthRoot.thy	Wed Oct 10 16:41:19 2012 +0200
     7.3 @@ -398,9 +398,9 @@
     7.4  
     7.5  lemma DERIV_real_root_generic:
     7.6    assumes "0 < n" and "x \<noteq> 0"
     7.7 -  and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
     7.8 -  and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
     7.9 -  and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
    7.10 +    and "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
    7.11 +    and "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
    7.12 +    and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
    7.13    shows "DERIV (root n) x :> D"
    7.14  using assms by (cases "even n", cases "0 < x",
    7.15    auto intro: DERIV_real_root[THEN DERIV_cong]
     8.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Wed Oct 10 16:18:27 2012 +0200
     8.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Wed Oct 10 16:41:19 2012 +0200
     8.3 @@ -84,7 +84,7 @@
     8.4  later use and is automatically propagated to all its interpretations.
     8.5  Here is another example: *}
     8.6  
     8.7 -statespace 'a varsX = vars [n=N, b=B] + vars + x::'a
     8.8 +statespace 'a varsX = NB: vars [n=N, b=B] + vars + x::'a
     8.9  
    8.10  text {* \noindent The state space @{text "varsX"} imports two copies
    8.11  of the state space @{text "vars"}, where one has the variables renamed
    8.12 @@ -179,7 +179,7 @@
    8.13  qed
    8.14  
    8.15  
    8.16 -statespace 'a dup = 'a foo [f=F, a=A] + 'a foo +
    8.17 +statespace 'a dup = FA: 'a foo [f=F, a=A] + 'a foo +
    8.18    x::int
    8.19  
    8.20  lemma (in dup)
     9.1 --- a/src/HOL/Statespace/state_space.ML	Wed Oct 10 16:18:27 2012 +0200
     9.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Oct 10 16:41:19 2012 +0200
     9.3 @@ -21,18 +21,18 @@
     9.4    val define_statespace :
     9.5       string list ->
     9.6       string ->
     9.7 -     (string list * bstring * (string * string) list) list ->
     9.8 +     ((string * bool) * (string list * bstring * (string * string) list)) list ->
     9.9       (string * string) list -> theory -> theory
    9.10    val define_statespace_i :
    9.11       string option ->
    9.12       string list ->
    9.13       string ->
    9.14 -     (typ list * bstring * (string * string) list) list ->
    9.15 +     ((string * bool) * (typ list * bstring * (string * string) list)) list ->
    9.16       (string * typ) list -> theory -> theory
    9.17  
    9.18    val statespace_decl :
    9.19       ((string list * bstring) *
    9.20 -       ((string list * xstring * (bstring * bstring) list) list *
    9.21 +       (((string * bool) * (string list * xstring * (bstring * bstring) list)) list *
    9.22          (bstring * string) list)) parser
    9.23  
    9.24  
    9.25 @@ -355,7 +355,7 @@
    9.26      val inst = map fst args ~~ Ts;
    9.27      val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
    9.28      val parent_comps =
    9.29 -      maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents;
    9.30 +      maps (fn (Ts',n,rs) => parent_components thy (map subst Ts', n, rs)) parents;
    9.31      val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
    9.32    in all_comps end;
    9.33  
    9.34 @@ -369,8 +369,8 @@
    9.35      val components' = map (fn (n,T) => (n,(T,full_name))) components;
    9.36      val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
    9.37  
    9.38 -    fun parent_expr (_,n,rs) = (suffix namespaceN n,((n,false),Expression.Positional rs));
    9.39 -        (* FIXME: a more specific renaming-prefix (including parameter names) may be nicer *)
    9.40 +    fun parent_expr (prefix, (_, n, rs)) =
    9.41 +      (suffix namespaceN n, (prefix, Expression.Positional rs));
    9.42      val parents_expr = map parent_expr parents;
    9.43      fun distinct_types Ts =
    9.44        let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty;
    9.45 @@ -386,14 +386,14 @@
    9.46      fun projectT T = valueT --> T;
    9.47      fun injectT T = T --> valueT;
    9.48      val locinsts = map (fn T => (project_injectL,
    9.49 -                    (("",false),Expression.Positional
    9.50 +                    ((encode_type T,false),Expression.Positional
    9.51                               [SOME (Free (project_name T,projectT T)),
    9.52                                SOME (Free ((inject_name T,injectT T)))]))) Ts;
    9.53      val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn),
    9.54                                       (Binding.name (inject_name T),NONE,NoSyn)]) Ts;
    9.55      val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts;
    9.56  
    9.57 -    fun interprete_parent_valuetypes (Ts, pname, _) thy =
    9.58 +    fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy =
    9.59        let
    9.60          val {args,types,...} =
    9.61               the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
    9.62 @@ -402,15 +402,15 @@
    9.63          val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
    9.64  
    9.65          val expr = ([(suffix valuetypesN name,
    9.66 -                     (("",false),Expression.Positional (map SOME pars)))],[]);
    9.67 +                     (prefix, Expression.Positional (map SOME pars)))],[]);
    9.68        in
    9.69          prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
    9.70            (suffix valuetypesN name, expr) thy
    9.71        end;
    9.72  
    9.73 -    fun interprete_parent (_, pname, rs) =
    9.74 +    fun interprete_parent (prefix, (_, pname, rs)) =
    9.75        let
    9.76 -        val expr = ([(pname, (("",false), Expression.Positional rs))],[])
    9.77 +        val expr = ([(pname, (prefix, Expression.Positional rs))],[])
    9.78        in prove_interpretation_in
    9.79             (fn ctxt => Locale.intro_locales_tac false ctxt [])
    9.80             (full_name, expr) end;
    9.81 @@ -449,7 +449,7 @@
    9.82       |> namespace_definition
    9.83             (suffix namespaceN name) nameT (parents_expr,[])
    9.84             (map fst parent_comps) (map fst components)
    9.85 -     |> Context.theory_map (add_statespace full_name args parents components [])
    9.86 +     |> Context.theory_map (add_statespace full_name args (map snd parents) components [])
    9.87       |> add_locale (suffix valuetypesN name) (locinsts,locs) []
    9.88       |> Proof_Context.theory_of
    9.89       |> fold interprete_parent_valuetypes parents
    9.90 @@ -495,8 +495,13 @@
    9.91  
    9.92      val ctxt = Proof_Context.init_global thy;
    9.93  
    9.94 -    fun add_parent (Ts,pname,rs) env =
    9.95 +    fun add_parent (prefix, (Ts, pname, rs)) env =
    9.96        let
    9.97 +        val prefix' =
    9.98 +          (case prefix of
    9.99 +            ("", mandatory) => (pname, mandatory)
   9.100 +          | _ => prefix);
   9.101 +
   9.102          val full_pname = Sign.full_bname thy pname;
   9.103          val {args,components,...} =
   9.104                (case get_statespace (Context.Theory thy) full_pname of
   9.105 @@ -526,8 +531,9 @@
   9.106  
   9.107          val rs' = map (AList.lookup (op =) rs o fst) components;
   9.108          val errs =err_insts @ err_dup_renamings @ err_rename_unknowns
   9.109 -      in if null errs then ((Ts',full_pname,rs'),env')
   9.110 -         else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
   9.111 +      in
   9.112 +        if null errs then ((prefix', (Ts', full_pname, rs')), env')
   9.113 +        else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
   9.114        end;
   9.115  
   9.116      val (parents',env) = fold_map add_parent parents [];
   9.117 @@ -562,7 +568,7 @@
   9.118      fun fst_eq ((x:string,_),(y,_)) = x = y;
   9.119      fun snd_eq ((_,t:typ),(_,u)) = t = u;
   9.120  
   9.121 -    val raw_parent_comps = maps (parent_components thy) parents';
   9.122 +    val raw_parent_comps = maps (parent_components thy o snd) parents';
   9.123      fun check_type (n,T) =
   9.124            (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
   9.125               []  => []
   9.126 @@ -687,8 +693,9 @@
   9.127  val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
   9.128  
   9.129  val parent =
   9.130 +  Parse_Spec.locale_prefix false --
   9.131    ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
   9.132 -    >> (fn ((insts, name), renames) => (insts,name, renames));
   9.133 +    >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
   9.134  
   9.135  in
   9.136  
    10.1 --- a/src/HOL/ex/Tarski.thy	Wed Oct 10 16:18:27 2012 +0200
    10.2 +++ b/src/HOL/ex/Tarski.thy	Wed Oct 10 16:41:19 2012 +0200
    10.3 @@ -119,7 +119,7 @@
    10.4  locale CL = S +
    10.5    assumes cl_co:  "cl : CompleteLattice"
    10.6  
    10.7 -sublocale CL < PO
    10.8 +sublocale CL < po: PO
    10.9  apply (simp_all add: A_def r_def)
   10.10  apply unfold_locales
   10.11  using cl_co unfolding CompleteLattice_def by auto
   10.12 @@ -130,7 +130,7 @@
   10.13    assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
   10.14    defines P_def: "P == fix f A"
   10.15  
   10.16 -sublocale CLF < CL
   10.17 +sublocale CLF < cl: CL
   10.18  apply (simp_all add: A_def r_def)
   10.19  apply unfold_locales
   10.20  using f_cl unfolding CLF_set_def by auto
    11.1 --- a/src/Pure/Isar/element.ML	Wed Oct 10 16:18:27 2012 +0200
    11.2 +++ b/src/Pure/Isar/element.ML	Wed Oct 10 16:41:19 2012 +0200
    11.3 @@ -493,9 +493,9 @@
    11.4    | init (Defines defs) = Context.map_proof (fn ctxt =>
    11.5        let
    11.6          val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
    11.7 -        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    11.8 -            let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
    11.9 -            in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
   11.10 +        val asms = defs' |> map (fn (b, (t, ps)) =>
   11.11 +            let val (_, t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
   11.12 +            in (t', (b, [(t', ps)])) end);
   11.13          val (_, ctxt') = ctxt
   11.14            |> fold Variable.auto_fixes (map #1 asms)
   11.15            |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
   11.16 @@ -507,7 +507,13 @@
   11.17  
   11.18  fun activate_i elem ctxt =
   11.19    let
   11.20 -    val elem' = map_ctxt_attrib Args.assignable elem;
   11.21 +    val elem' =
   11.22 +      (case map_ctxt_attrib Args.assignable elem of
   11.23 +        Defines defs =>
   11.24 +          Defines (defs |> map (fn ((a, atts), (t, ps)) =>
   11.25 +            ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
   11.26 +              (t, ps))))
   11.27 +      | e => e);
   11.28      val ctxt' = Context.proof_map (init elem') ctxt;
   11.29    in (map_ctxt_attrib Args.closure elem', ctxt') end;
   11.30  
    12.1 --- a/src/Pure/Isar/expression.ML	Wed Oct 10 16:18:27 2012 +0200
    12.2 +++ b/src/Pure/Isar/expression.ML	Wed Oct 10 16:41:19 2012 +0200
    12.3 @@ -527,11 +527,11 @@
    12.4      val b' = norm_term env b;
    12.5      fun err msg = error (msg ^ ": " ^ quote y);
    12.6    in
    12.7 -    case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
    12.8 -      [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) |
    12.9 -      dups => if forall (fn (_, b'') => b' aconv b'') dups
   12.10 -        then (xs, env, eqs)
   12.11 -        else err "Attempt to redefine variable"
   12.12 +    (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
   12.13 +      [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
   12.14 +    | dups =>
   12.15 +        if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs)
   12.16 +        else err "Attempt to redefine variable")
   12.17    end;
   12.18  
   12.19  (* text has the following structure:
    13.1 --- a/src/Pure/Isar/local_defs.ML	Wed Oct 10 16:18:27 2012 +0200
    13.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Oct 10 16:41:19 2012 +0200
    13.3 @@ -89,16 +89,14 @@
    13.4  fun add_defs defs ctxt =
    13.5    let
    13.6      val ((xs, mxs), specs) = defs |> split_list |>> split_list;
    13.7 -    val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
    13.8 -    val names = map2 Thm.def_binding_optional xs bfacts;
    13.9 +    val (bs, rhss) = specs |> split_list;
   13.10      val eqs = mk_def ctxt (xs ~~ rhss);
   13.11      val lhss = map (fst o Logic.dest_equals) eqs;
   13.12    in
   13.13      ctxt
   13.14      |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
   13.15      |> fold Variable.declare_term eqs
   13.16 -    |> Proof_Context.add_assms_i def_export
   13.17 -      (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
   13.18 +    |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
   13.19      |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   13.20    end;
   13.21  
    14.1 --- a/src/Pure/Isar/parse_spec.ML	Wed Oct 10 16:18:27 2012 +0200
    14.2 +++ b/src/Pure/Isar/parse_spec.ML	Wed Oct 10 16:41:19 2012 +0200
    14.3 @@ -24,8 +24,9 @@
    14.4    val locale_fixes: (binding * string option * mixfix) list parser
    14.5    val locale_insts: (string option list * (Attrib.binding * string) list) parser
    14.6    val class_expression: string list parser
    14.7 +  val locale_prefix: bool -> (string * bool) parser
    14.8 +  val locale_keyword: string parser
    14.9    val locale_expression: bool -> Expression.expression parser
   14.10 -  val locale_keyword: string parser
   14.11    val context_element: Element.context parser
   14.12    val statement: (Attrib.binding * (string * string list) list) list parser
   14.13    val general_statement: (Element.context list * Element.statement) parser
   14.14 @@ -113,17 +114,19 @@
   14.15  fun plus1_unless test scan =
   14.16    scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
   14.17  
   14.18 -fun prefix mandatory =
   14.19 -  Parse.name --
   14.20 -    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
   14.21 -    Parse.$$$ ":";
   14.22 -
   14.23  val instance = Parse.where_ |--
   14.24    Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
   14.25    Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
   14.26  
   14.27  in
   14.28  
   14.29 +fun locale_prefix mandatory =
   14.30 +  Scan.optional
   14.31 +    (Parse.name --
   14.32 +      (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
   14.33 +      Parse.$$$ ":")
   14.34 +    ("", false);
   14.35 +
   14.36  val locale_keyword =
   14.37    Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   14.38    Parse.$$$ "defines" || Parse.$$$ "notes";
   14.39 @@ -133,7 +136,7 @@
   14.40  fun locale_expression mandatory =
   14.41    let
   14.42      val expr2 = Parse.position Parse.xname;
   14.43 -    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
   14.44 +    val expr1 = locale_prefix mandatory -- expr2 --
   14.45        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   14.46      val expr0 = plus1_unless locale_keyword expr1;
   14.47    in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
    15.1 --- a/src/Pure/Isar/proof.ML	Wed Oct 10 16:18:27 2012 +0200
    15.2 +++ b/src/Pure/Isar/proof.ML	Wed Oct 10 16:41:19 2012 +0200
    15.3 @@ -643,7 +643,11 @@
    15.4      |>> map (fn (x, _, mx) => (x, mx))
    15.5      |-> (fn vars =>
    15.6        map_context_result (prep_binds false (map swap raw_rhss))
    15.7 -      #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
    15.8 +      #-> (fn rhss =>
    15.9 +        let
   15.10 +          val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
   15.11 +            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
   15.12 +        in map_context_result (Local_Defs.add_defs defs) end))
   15.13      |-> (set_facts o map (#2 o #2))
   15.14    end;
   15.15  
    16.1 --- a/src/Pure/Isar/proof_context.ML	Wed Oct 10 16:18:27 2012 +0200
    16.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Oct 10 16:41:19 2012 +0200
    16.3 @@ -938,8 +938,8 @@
    16.4  local
    16.5  
    16.6  fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
    16.7 -  | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
    16.8 -      (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
    16.9 +  | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts
   16.10 +      (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd);
   16.11  
   16.12  in
   16.13  
   16.14 @@ -952,12 +952,12 @@
   16.15      val (res, ctxt') = fold_map app facts ctxt;
   16.16      val thms = Global_Theory.name_thms false false name (flat res);
   16.17      val Mode {stmt, ...} = get_mode ctxt;
   16.18 -  in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
   16.19 +  in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end);
   16.20  
   16.21 -fun put_thms do_props thms ctxt = ctxt
   16.22 +fun put_thms index thms ctxt = ctxt
   16.23    |> map_naming (K Name_Space.local_naming)
   16.24    |> Context_Position.set_visible false
   16.25 -  |> update_thms do_props (apfst Binding.name thms)
   16.26 +  |> update_thms {strict = false, index = index} (apfst Binding.name thms)
   16.27    |> Context_Position.restore_visible ctxt
   16.28    |> restore_naming ctxt;
   16.29  
    17.1 --- a/src/Pure/facts.ML	Wed Oct 10 16:18:27 2012 +0200
    17.2 +++ b/src/Pure/facts.ML	Wed Oct 10 16:41:19 2012 +0200
    17.3 @@ -32,8 +32,8 @@
    17.4    val props: T -> thm list
    17.5    val could_unify: T -> term -> thm list
    17.6    val merge: T * T -> T
    17.7 -  val add_global: Context.generic -> binding * thm list -> T -> string * T
    17.8 -  val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
    17.9 +  val add_static: Context.generic -> {strict: bool, index: bool} ->
   17.10 +    binding * thm list -> T -> string * T
   17.11    val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
   17.12    val del: string -> T -> T
   17.13    val hide: bool -> string -> T -> T
   17.14 @@ -188,26 +188,15 @@
   17.15  
   17.16  (* add static entries *)
   17.17  
   17.18 -local
   17.19 -
   17.20 -fun add context strict do_props (b, ths) (Facts {facts, props}) =
   17.21 +fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
   17.22    let
   17.23      val (name, facts') =
   17.24        if Binding.is_empty b then ("", facts)
   17.25        else Name_Space.define context strict (b, Static ths) facts;
   17.26 -    val props' =
   17.27 -      if do_props
   17.28 -      then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
   17.29 -      else props;
   17.30 +    val props' = props
   17.31 +      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
   17.32    in (name, make_facts facts' props') end;
   17.33  
   17.34 -in
   17.35 -
   17.36 -fun add_global context = add context true false;
   17.37 -fun add_local context = add context false;
   17.38 -
   17.39 -end;
   17.40 -
   17.41  
   17.42  (* add dynamic entries *)
   17.43  
    18.1 --- a/src/Pure/global_theory.ML	Wed Oct 10 16:18:27 2012 +0200
    18.2 +++ b/src/Pure/global_theory.ML	Wed Oct 10 16:41:19 2012 +0200
    18.3 @@ -134,7 +134,8 @@
    18.4        val name = Sign.full_name thy b;
    18.5        val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
    18.6        val thms'' = map (Thm.transfer thy') thms';
    18.7 -      val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
    18.8 +      val thy'' = thy' |> Data.map
    18.9 +        (Facts.add_static (Context.Theory thy') {strict = true, index = false} (b, thms'') #> snd);
   18.10      in (thms'', thy'') end;
   18.11  
   18.12  
    19.1 --- a/src/Tools/induct.ML	Wed Oct 10 16:18:27 2012 +0200
    19.2 +++ b/src/Tools/induct.ML	Wed Oct 10 16:41:19 2012 +0200
    19.3 @@ -705,15 +705,15 @@
    19.4      fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
    19.5        | add (SOME (SOME x, (t, _))) ctxt =
    19.6            let val ([(lhs, (_, th))], ctxt') =
    19.7 -            Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
    19.8 +            Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
    19.9            in ((SOME lhs, [th]), ctxt') end
   19.10        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
   19.11        | add (SOME (NONE, (t, _))) ctxt =
   19.12            let
   19.13              val (s, _) = Name.variant "x" (Variable.names_of ctxt);
   19.14 -            val ([(lhs, (_, th))], ctxt') =
   19.15 -              Local_Defs.add_defs [((Binding.name s, NoSyn),
   19.16 -                (Thm.empty_binding, t))] ctxt
   19.17 +            val x = Binding.name s;
   19.18 +            val ([(lhs, (_, th))], ctxt') = ctxt
   19.19 +              |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
   19.20            in ((SOME lhs, [th]), ctxt') end
   19.21        | add NONE ctxt = ((NONE, []), ctxt);
   19.22    in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
    20.1 --- a/src/ZF/ex/Group.thy	Wed Oct 10 16:18:27 2012 +0200
    20.2 +++ b/src/ZF/ex/Group.thy	Wed Oct 10 16:41:19 2012 +0200
    20.3 @@ -203,11 +203,11 @@
    20.4  qed
    20.5  
    20.6  lemma (in group) inv_comm:
    20.7 -  assumes inv: "x \<cdot> y = \<one>"
    20.8 +  assumes "x \<cdot> y = \<one>"
    20.9        and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"
   20.10    shows "y \<cdot> x = \<one>"
   20.11  proof -
   20.12 -  from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv)
   20.13 +  from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: assms)
   20.14    with G show ?thesis by (simp del: r_one add: m_assoc)
   20.15  qed
   20.16  
   20.17 @@ -490,11 +490,12 @@
   20.18  
   20.19  lemma (in group) subgroupI:
   20.20    assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"
   20.21 -    and inv: "!!a. a \<in> H ==> inv a \<in> H"
   20.22 -    and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
   20.23 +    and "!!a. a \<in> H ==> inv a \<in> H"
   20.24 +    and "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
   20.25    shows "subgroup(H,G)"
   20.26  proof (simp add: subgroup_def assms)
   20.27 -  show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)
   20.28 +  show "\<one> \<in> H"
   20.29 +    by (rule one_in_subset) (auto simp only: assms)
   20.30  qed
   20.31  
   20.32  
   20.33 @@ -595,7 +596,7 @@
   20.34    "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
   20.35  
   20.36  
   20.37 -locale normal = subgroup + group +
   20.38 +locale normal = subgroup: subgroup + group +
   20.39    assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
   20.40  
   20.41  notation