merged
authorhaftmann
Wed Sep 30 09:25:18 2009 +0200 (2009-09-30)
changeset 32775d498770eefdc
parent 32771 995b9c763c66
parent 32774 461afcc6acb8
child 32776 1504f9c2d060
merged
NEWS
     1.1 --- a/NEWS	Wed Sep 30 00:57:28 2009 +0200
     1.2 +++ b/NEWS	Wed Sep 30 09:25:18 2009 +0200
     1.3 @@ -18,6 +18,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Most rules produced by inductive and datatype package
     1.8 +have mandatory prefixes.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * New proof method "smt" for a combination of first-order logic
    1.12  with equality, linear and nonlinear (natural/integer/real)
    1.13  arithmetic, and fixed-size bitvectors; there is also basic
     2.1 --- a/src/HOL/Nat.thy	Wed Sep 30 00:57:28 2009 +0200
     2.2 +++ b/src/HOL/Nat.thy	Wed Sep 30 09:25:18 2009 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4    assumes "P 0"
     2.5      and "\<And>n. P n \<Longrightarrow> P (Suc n)"
     2.6    shows "P n"
     2.7 -  using assms by (rule nat.induct) 
     2.8 +  using assms by (rule nat.induct)
     2.9  
    2.10  declare nat.exhaust [case_names 0 Suc, cases type: nat]
    2.11  
     3.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 30 00:57:28 2009 +0200
     3.2 +++ b/src/HOL/Tools/inductive.ML	Wed Sep 30 09:25:18 2009 +0200
     3.3 @@ -683,7 +683,7 @@
     3.4        elims raw_induct ctxt =
     3.5    let
     3.6      val rec_name = Binding.name_of rec_binding;
     3.7 -    val rec_qualified = Binding.qualify false rec_name;
     3.8 +    fun rec_qualified qualified = Binding.qualify qualified rec_name;
     3.9      val intr_names = map Binding.name_of intr_bindings;
    3.10      val ind_case_names = RuleCases.case_names intr_names;
    3.11      val induct =
    3.12 @@ -698,29 +698,29 @@
    3.13      val (intrs', ctxt1) =
    3.14        ctxt |>
    3.15        LocalTheory.notes kind
    3.16 -        (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
    3.17 +        (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
    3.18             [Attrib.internal (K (ContextRules.intro_query NONE)),
    3.19              Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
    3.20        map (hd o snd);
    3.21      val (((_, elims'), (_, [induct'])), ctxt2) =
    3.22        ctxt1 |>
    3.23 -      LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
    3.24 +      LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    3.25        fold_map (fn (name, (elim, cases)) =>
    3.26 -        LocalTheory.note kind ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "cases"),
    3.27 +        LocalTheory.note kind ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
    3.28            [Attrib.internal (K (RuleCases.case_names cases)),
    3.29             Attrib.internal (K (RuleCases.consumes 1)),
    3.30             Attrib.internal (K (Induct.cases_pred name)),
    3.31             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    3.32          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    3.33        LocalTheory.note kind
    3.34 -        ((rec_qualified (Binding.name (coind_prefix coind ^ "induct")),
    3.35 +        ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
    3.36            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
    3.37  
    3.38      val ctxt3 = if no_ind orelse coind then ctxt2 else
    3.39        let val inducts = cnames ~~ Project_Rule.projects ctxt2 (1 upto length cnames) induct'
    3.40        in
    3.41          ctxt2 |>
    3.42 -        LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []),
    3.43 +        LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
    3.44            inducts |> map (fn (name, th) => ([th],
    3.45              [Attrib.internal (K ind_case_names),
    3.46               Attrib.internal (K (RuleCases.consumes 1)),