--- a/src/Cube/Cube.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Cube/Cube.thy Wed Oct 10 16:19:52 2012 +0200
@@ -10,6 +10,15 @@
setup Pure_Thy.old_appl_syntax_setup
+ML {*
+ structure Rules = Named_Thms
+ (
+ val name = @{binding rules}
+ val description = "Cube inference rules"
+ )
+*}
+setup Rules.setup
+
typedecl "term"
typedecl "context"
typedecl typing
@@ -72,8 +81,7 @@
beta: "Abs(A, f)^a == f(a)"
-lemmas simple = s_b strip_s strip_b app lam_ss pi_ss
-lemmas rules = simple
+lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
lemma imp_elim:
assumes "f:A\<rightarrow>B" and "a:A" and "f^a:B ==> PROP P"
@@ -90,7 +98,7 @@
==> Abs(A,f) : Prod(A,B)"
begin
-lemmas rules = simple lam_bs pi_bs
+lemmas [rules] = lam_bs pi_bs
end
@@ -102,7 +110,7 @@
==> Abs(A,f) : Prod(A,B)"
begin
-lemmas rules = simple lam_bb pi_bb
+lemmas [rules] = lam_bb pi_bb
end
@@ -113,7 +121,7 @@
==> Abs(A,f) : Prod(A,B)"
begin
-lemmas rules = simple lam_sb pi_sb
+lemmas [rules] = lam_sb pi_sb
end
@@ -121,7 +129,7 @@
locale LP2 = LP + L2
begin
-lemmas rules = simple lam_bs pi_bs lam_sb pi_sb
+lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
end
@@ -129,7 +137,7 @@
locale Lomega2 = L2 + Lomega
begin
-lemmas rules = simple lam_bs pi_bs lam_bb pi_bb
+lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
end
@@ -137,7 +145,7 @@
locale LPomega = LP + Lomega
begin
-lemmas rules = simple lam_bb pi_bb lam_sb pi_sb
+lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
end
@@ -145,7 +153,7 @@
locale CC = L2 + LP + Lomega
begin
-lemmas rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
+lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
end
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Oct 10 16:19:52 2012 +0200
@@ -104,7 +104,7 @@
end
print_locale! logic
-locale use_decl = logic + semi "op ||"
+locale use_decl = l: logic + semi "op ||"
print_locale! use_decl thm use_decl_def
locale extra_type =
--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 16:19:52 2012 +0200
@@ -273,7 +273,7 @@
lemma embed_underS:
-assumes WELL: "Well_order r" and WELL: "Well_order r'" and
+assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and IN: "a \<in> Field r"
shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
proof-
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Oct 10 16:19:52 2012 +0200
@@ -452,7 +452,7 @@
assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
and between_same: "between x x = x"
-sublocale constr_dense_linorder < dense_linorder
+sublocale constr_dense_linorder < dlo: dense_linorder
apply unfold_locales
using gt_ex lt_ex between_less
apply auto
--- a/src/HOL/Finite_Set.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/Finite_Set.thy Wed Oct 10 16:19:52 2012 +0200
@@ -1757,7 +1757,7 @@
locale folding_image_simple_idem = folding_image_simple +
assumes idem: "x * x = x"
-sublocale folding_image_simple_idem < semilattice proof
+sublocale folding_image_simple_idem < semilattice: semilattice proof
qed (fact idem)
context folding_image_simple_idem
@@ -1898,7 +1898,7 @@
locale folding_one_idem = folding_one +
assumes idem: "x * x = x"
-sublocale folding_one_idem < semilattice proof
+sublocale folding_one_idem < semilattice: semilattice proof
qed (fact idem)
context folding_one_idem
--- a/src/HOL/Library/Univ_Poly.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Wed Oct 10 16:19:52 2012 +0200
@@ -414,7 +414,6 @@
apply (auto simp add: poly_exp poly_mult)
done
-lemma (in semiring_1) one_neq_zero[simp]: "1 \<noteq> 0" using zero_neq_one by blast
lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \<noteq> poly []"
apply (simp add: fun_eq)
apply (rule_tac x = "minus one a" in exI)
--- a/src/HOL/NthRoot.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/NthRoot.thy Wed Oct 10 16:19:52 2012 +0200
@@ -398,9 +398,9 @@
lemma DERIV_real_root_generic:
assumes "0 < n" and "x \<noteq> 0"
- and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
- and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
- and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+ and "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+ and "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
+ and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
shows "DERIV (root n) x :> D"
using assms by (cases "even n", cases "0 < x",
auto intro: DERIV_real_root[THEN DERIV_cong]
--- a/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 10 16:19:52 2012 +0200
@@ -84,7 +84,7 @@
later use and is automatically propagated to all its interpretations.
Here is another example: *}
-statespace 'a varsX = vars [n=N, b=B] + vars + x::'a
+statespace 'a varsX = NB: vars [n=N, b=B] + vars + x::'a
text {* \noindent The state space @{text "varsX"} imports two copies
of the state space @{text "vars"}, where one has the variables renamed
@@ -179,7 +179,7 @@
qed
-statespace 'a dup = 'a foo [f=F, a=A] + 'a foo +
+statespace 'a dup = FA: 'a foo [f=F, a=A] + 'a foo +
x::int
lemma (in dup)
--- a/src/HOL/Statespace/state_space.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Oct 10 16:19:52 2012 +0200
@@ -21,18 +21,18 @@
val define_statespace :
string list ->
string ->
- (string list * bstring * (string * string) list) list ->
+ ((string * bool) * (string list * bstring * (string * string) list)) list ->
(string * string) list -> theory -> theory
val define_statespace_i :
string option ->
string list ->
string ->
- (typ list * bstring * (string * string) list) list ->
+ ((string * bool) * (typ list * bstring * (string * string) list)) list ->
(string * typ) list -> theory -> theory
val statespace_decl :
((string list * bstring) *
- ((string list * xstring * (bstring * bstring) list) list *
+ (((string * bool) * (string list * xstring * (bstring * bstring) list)) list *
(bstring * string) list)) parser
@@ -355,7 +355,7 @@
val inst = map fst args ~~ Ts;
val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
val parent_comps =
- maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents;
+ maps (fn (Ts',n,rs) => parent_components thy (map subst Ts', n, rs)) parents;
val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
in all_comps end;
@@ -369,8 +369,8 @@
val components' = map (fn (n,T) => (n,(T,full_name))) components;
val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
- fun parent_expr (_,n,rs) = (suffix namespaceN n,((n,false),Expression.Positional rs));
- (* FIXME: a more specific renaming-prefix (including parameter names) may be nicer *)
+ fun parent_expr (prefix, (_, n, rs)) =
+ (suffix namespaceN n, (prefix, Expression.Positional rs));
val parents_expr = map parent_expr parents;
fun distinct_types Ts =
let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty;
@@ -386,14 +386,14 @@
fun projectT T = valueT --> T;
fun injectT T = T --> valueT;
val locinsts = map (fn T => (project_injectL,
- (("",false),Expression.Positional
+ ((encode_type T,false),Expression.Positional
[SOME (Free (project_name T,projectT T)),
SOME (Free ((inject_name T,injectT T)))]))) Ts;
val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn),
(Binding.name (inject_name T),NONE,NoSyn)]) Ts;
val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts;
- fun interprete_parent_valuetypes (Ts, pname, _) thy =
+ fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy =
let
val {args,types,...} =
the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
@@ -402,15 +402,15 @@
val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
val expr = ([(suffix valuetypesN name,
- (("",false),Expression.Positional (map SOME pars)))],[]);
+ (prefix, Expression.Positional (map SOME pars)))],[]);
in
prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
(suffix valuetypesN name, expr) thy
end;
- fun interprete_parent (_, pname, rs) =
+ fun interprete_parent (prefix, (_, pname, rs)) =
let
- val expr = ([(pname, (("",false), Expression.Positional rs))],[])
+ val expr = ([(pname, (prefix, Expression.Positional rs))],[])
in prove_interpretation_in
(fn ctxt => Locale.intro_locales_tac false ctxt [])
(full_name, expr) end;
@@ -449,7 +449,7 @@
|> namespace_definition
(suffix namespaceN name) nameT (parents_expr,[])
(map fst parent_comps) (map fst components)
- |> Context.theory_map (add_statespace full_name args parents components [])
+ |> Context.theory_map (add_statespace full_name args (map snd parents) components [])
|> add_locale (suffix valuetypesN name) (locinsts,locs) []
|> Proof_Context.theory_of
|> fold interprete_parent_valuetypes parents
@@ -495,8 +495,13 @@
val ctxt = Proof_Context.init_global thy;
- fun add_parent (Ts,pname,rs) env =
+ fun add_parent (prefix, (Ts, pname, rs)) env =
let
+ val prefix' =
+ (case prefix of
+ ("", mandatory) => (pname, mandatory)
+ | _ => prefix);
+
val full_pname = Sign.full_bname thy pname;
val {args,components,...} =
(case get_statespace (Context.Theory thy) full_pname of
@@ -526,8 +531,9 @@
val rs' = map (AList.lookup (op =) rs o fst) components;
val errs =err_insts @ err_dup_renamings @ err_rename_unknowns
- in if null errs then ((Ts',full_pname,rs'),env')
- else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
+ in
+ if null errs then ((prefix', (Ts', full_pname, rs')), env')
+ else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
end;
val (parents',env) = fold_map add_parent parents [];
@@ -562,7 +568,7 @@
fun fst_eq ((x:string,_),(y,_)) = x = y;
fun snd_eq ((_,t:typ),(_,u)) = t = u;
- val raw_parent_comps = maps (parent_components thy) parents';
+ val raw_parent_comps = maps (parent_components thy o snd) parents';
fun check_type (n,T) =
(case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
[] => []
@@ -687,8 +693,9 @@
val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
val parent =
+ Parse_Spec.locale_prefix false --
((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
- >> (fn ((insts, name), renames) => (insts,name, renames));
+ >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
in
--- a/src/HOL/ex/Tarski.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/ex/Tarski.thy Wed Oct 10 16:19:52 2012 +0200
@@ -119,7 +119,7 @@
locale CL = S +
assumes cl_co: "cl : CompleteLattice"
-sublocale CL < PO
+sublocale CL < po: PO
apply (simp_all add: A_def r_def)
apply unfold_locales
using cl_co unfolding CompleteLattice_def by auto
@@ -130,7 +130,7 @@
assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
defines P_def: "P == fix f A"
-sublocale CLF < CL
+sublocale CLF < cl: CL
apply (simp_all add: A_def r_def)
apply unfold_locales
using f_cl unfolding CLF_set_def by auto
--- a/src/Pure/Isar/element.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Pure/Isar/element.ML Wed Oct 10 16:19:52 2012 +0200
@@ -493,9 +493,9 @@
| init (Defines defs) = Context.map_proof (fn ctxt =>
let
val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
- val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
- let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
- in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
+ val asms = defs' |> map (fn (b, (t, ps)) =>
+ let val (_, t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
+ in (t', (b, [(t', ps)])) end);
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (map #1 asms)
|> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
@@ -507,7 +507,13 @@
fun activate_i elem ctxt =
let
- val elem' = map_ctxt_attrib Args.assignable elem;
+ val elem' =
+ (case map_ctxt_attrib Args.assignable elem of
+ Defines defs =>
+ Defines (defs |> map (fn ((a, atts), (t, ps)) =>
+ ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
+ (t, ps))))
+ | e => e);
val ctxt' = Context.proof_map (init elem') ctxt;
in (map_ctxt_attrib Args.closure elem', ctxt') end;
--- a/src/Pure/Isar/expression.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Pure/Isar/expression.ML Wed Oct 10 16:19:52 2012 +0200
@@ -527,11 +527,11 @@
val b' = norm_term env b;
fun err msg = error (msg ^ ": " ^ quote y);
in
- case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
- [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) |
- dups => if forall (fn (_, b'') => b' aconv b'') dups
- then (xs, env, eqs)
- else err "Attempt to redefine variable"
+ (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
+ [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
+ | dups =>
+ if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs)
+ else err "Attempt to redefine variable")
end;
(* text has the following structure:
--- a/src/Pure/Isar/local_defs.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Pure/Isar/local_defs.ML Wed Oct 10 16:19:52 2012 +0200
@@ -89,16 +89,14 @@
fun add_defs defs ctxt =
let
val ((xs, mxs), specs) = defs |> split_list |>> split_list;
- val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
- val names = map2 Thm.def_binding_optional xs bfacts;
+ val (bs, rhss) = specs |> split_list;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
in
ctxt
|> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
|> fold Variable.declare_term eqs
- |> Proof_Context.add_assms_i def_export
- (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
+ |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
|>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
end;
--- a/src/Pure/Isar/parse_spec.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Pure/Isar/parse_spec.ML Wed Oct 10 16:19:52 2012 +0200
@@ -24,8 +24,9 @@
val locale_fixes: (binding * string option * mixfix) list parser
val locale_insts: (string option list * (Attrib.binding * string) list) parser
val class_expression: string list parser
+ val locale_prefix: bool -> (string * bool) parser
+ val locale_keyword: string parser
val locale_expression: bool -> Expression.expression parser
- val locale_keyword: string parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
val general_statement: (Element.context list * Element.statement) parser
@@ -113,17 +114,19 @@
fun plus1_unless test scan =
scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
-fun prefix mandatory =
- Parse.name --
- (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
- Parse.$$$ ":";
-
val instance = Parse.where_ |--
Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
in
+fun locale_prefix mandatory =
+ Scan.optional
+ (Parse.name --
+ (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
+ Parse.$$$ ":")
+ ("", false);
+
val locale_keyword =
Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
Parse.$$$ "defines" || Parse.$$$ "notes";
@@ -133,7 +136,7 @@
fun locale_expression mandatory =
let
val expr2 = Parse.position Parse.xname;
- val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
+ val expr1 = locale_prefix mandatory -- expr2 --
Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
val expr0 = plus1_unless locale_keyword expr1;
in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
--- a/src/Pure/Isar/proof.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Pure/Isar/proof.ML Wed Oct 10 16:19:52 2012 +0200
@@ -643,7 +643,11 @@
|>> map (fn (x, _, mx) => (x, mx))
|-> (fn vars =>
map_context_result (prep_binds false (map swap raw_rhss))
- #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
+ #-> (fn rhss =>
+ let
+ val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
+ ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
+ in map_context_result (Local_Defs.add_defs defs) end))
|-> (set_facts o map (#2 o #2))
end;
--- a/src/Pure/Isar/proof_context.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Oct 10 16:19:52 2012 +0200
@@ -938,8 +938,8 @@
local
fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
- | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
- (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
+ | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts
+ (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd);
in
@@ -952,12 +952,12 @@
val (res, ctxt') = fold_map app facts ctxt;
val thms = Global_Theory.name_thms false false name (flat res);
val Mode {stmt, ...} = get_mode ctxt;
- in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
+ in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end);
-fun put_thms do_props thms ctxt = ctxt
+fun put_thms index thms ctxt = ctxt
|> map_naming (K Name_Space.local_naming)
|> Context_Position.set_visible false
- |> update_thms do_props (apfst Binding.name thms)
+ |> update_thms {strict = false, index = index} (apfst Binding.name thms)
|> Context_Position.restore_visible ctxt
|> restore_naming ctxt;
--- a/src/Pure/facts.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Pure/facts.ML Wed Oct 10 16:19:52 2012 +0200
@@ -32,8 +32,8 @@
val props: T -> thm list
val could_unify: T -> term -> thm list
val merge: T * T -> T
- val add_global: Context.generic -> binding * thm list -> T -> string * T
- val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
+ val add_static: Context.generic -> {strict: bool, index: bool} ->
+ binding * thm list -> T -> string * T
val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
@@ -188,26 +188,15 @@
(* add static entries *)
-local
-
-fun add context strict do_props (b, ths) (Facts {facts, props}) =
+fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
let
val (name, facts') =
if Binding.is_empty b then ("", facts)
else Name_Space.define context strict (b, Static ths) facts;
- val props' =
- if do_props
- then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
- else props;
+ val props' = props
+ |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
in (name, make_facts facts' props') end;
-in
-
-fun add_global context = add context true false;
-fun add_local context = add context false;
-
-end;
-
(* add dynamic entries *)
--- a/src/Pure/global_theory.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Pure/global_theory.ML Wed Oct 10 16:19:52 2012 +0200
@@ -134,7 +134,8 @@
val name = Sign.full_name thy b;
val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
val thms'' = map (Thm.transfer thy') thms';
- val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
+ val thy'' = thy' |> Data.map
+ (Facts.add_static (Context.Theory thy') {strict = true, index = false} (b, thms'') #> snd);
in (thms'', thy'') end;
--- a/src/Tools/induct.ML Wed Oct 10 13:30:50 2012 +0200
+++ b/src/Tools/induct.ML Wed Oct 10 16:19:52 2012 +0200
@@ -705,15 +705,15 @@
fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
| add (SOME (SOME x, (t, _))) ctxt =
let val ([(lhs, (_, th))], ctxt') =
- Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
+ Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
| add (SOME (NONE, (t, _))) ctxt =
let
val (s, _) = Name.variant "x" (Variable.names_of ctxt);
- val ([(lhs, (_, th))], ctxt') =
- Local_Defs.add_defs [((Binding.name s, NoSyn),
- (Thm.empty_binding, t))] ctxt
+ val x = Binding.name s;
+ val ([(lhs, (_, th))], ctxt') = ctxt
+ |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
in ((SOME lhs, [th]), ctxt') end
| add NONE ctxt = ((NONE, []), ctxt);
in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
--- a/src/ZF/ex/Group.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/ZF/ex/Group.thy Wed Oct 10 16:19:52 2012 +0200
@@ -203,11 +203,11 @@
qed
lemma (in group) inv_comm:
- assumes inv: "x \<cdot> y = \<one>"
+ assumes "x \<cdot> y = \<one>"
and G: "x \<in> carrier(G)" "y \<in> carrier(G)"
shows "y \<cdot> x = \<one>"
proof -
- from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv)
+ from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: assms)
with G show ?thesis by (simp del: r_one add: m_assoc)
qed
@@ -490,11 +490,12 @@
lemma (in group) subgroupI:
assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"
- and inv: "!!a. a \<in> H ==> inv a \<in> H"
- and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
+ and "!!a. a \<in> H ==> inv a \<in> H"
+ and "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
shows "subgroup(H,G)"
proof (simp add: subgroup_def assms)
- show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)
+ show "\<one> \<in> H"
+ by (rule one_in_subset) (auto simp only: assms)
qed
@@ -595,7 +596,7 @@
"set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
-locale normal = subgroup + group +
+locale normal = subgroup: subgroup + group +
assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
notation