Experimental support for rewrite morphisms in locale instances.
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Jan 16 15:53:42 2018 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Jan 16 19:28:05 2018 +0100
@@ -521,6 +521,15 @@
x.lor_triv
+subsection \<open>Rewrite morphisms in expressions\<close>
+
+interpretation y: logic_o "(\<or>)" "Not" replaces bool_logic_o2: "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y"
+proof -
+ show bool_logic_o: "PROP logic_o((\<or>), Not)" by unfold_locales fast+
+ show "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y" unfolding logic_o.lor_o_def [OF bool_logic_o] by fast
+qed
+
+
subsection \<open>Inheritance of rewrite morphisms\<close>
locale reflexive =
--- a/src/HOL/Statespace/state_space.ML Tue Jan 16 15:53:42 2018 +0100
+++ b/src/HOL/Statespace/state_space.ML Tue Jan 16 19:28:05 2018 +0100
@@ -324,7 +324,7 @@
val components' = map (fn (n,T) => (n,(T,full_name))) components;
fun parent_expr (prefix, (_, n, rs)) =
- (suffix namespaceN n, (prefix, Expression.Positional 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;
@@ -340,9 +340,9 @@
fun projectT T = valueT --> T;
fun injectT T = T --> valueT;
val locinsts = map (fn T => (project_injectL,
- ((encode_type T,false),Expression.Positional
+ ((encode_type T,false),(Expression.Positional
[SOME (Free (project_name T,projectT T)),
- SOME (Free ((inject_name T,injectT T)))]))) Ts;
+ 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;
@@ -356,7 +356,7 @@
val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
val expr = ([(suffix valuetypesN name,
- (prefix, Expression.Positional (map SOME pars)))],[]);
+ (prefix, (Expression.Positional (map SOME pars),[])))],[]);
in
prove_interpretation_in (fn ctxt => ALLGOALS (solve_tac ctxt (Assumption.all_prems_of ctxt)))
(suffix valuetypesN name, expr) thy
@@ -364,7 +364,7 @@
fun interprete_parent (prefix, (_, pname, rs)) =
let
- val expr = ([(pname, (prefix, 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;
@@ -408,8 +408,8 @@
|> Proof_Context.theory_of
|> fold interprete_parent_valuetypes parents
|> add_locale_cmd name
- ([(suffix namespaceN full_name ,(("",false),Expression.Named [])),
- (suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate
+ ([(suffix namespaceN full_name ,(("",false),(Expression.Named [],[]))),
+ (suffix valuetypesN full_name,(("",false),(Expression.Named [],[])))],[]) fixestate
|> Proof_Context.theory_of
|> fold interprete_parent parents
|> add_declaration full_name (declare_declinfo components')
--- a/src/Pure/Isar/class_declaration.ML Tue Jan 16 15:53:42 2018 +0100
+++ b/src/Pure/Isar/class_declaration.ML Tue Jan 16 19:28:05 2018 +0100
@@ -38,9 +38,9 @@
(Symtab.empty, Symtab.make param_map_inst);
val typ_morph = Element.inst_morphism thy
(Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
- val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
+ val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = empty_ctxt
|> Expression.cert_goal_expression ([(class, (("", false),
- Expression.Named param_map_const))], []);
+ (Expression.Named param_map_const, [])))], []);
val (props, inst_morph) =
if null param_map
then (raw_props |> map (Morphism.term typ_morph),
@@ -156,7 +156,7 @@
(* preprocessing elements, retrieving base sort from type-checked elements *)
val raw_supexpr =
- (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
+ (map (fn sup => (sup, (("", false), (Expression.Positional [], [])))) sups, []);
val init_class_body =
fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
#> Class.redeclare_operations thy sups
@@ -192,7 +192,7 @@
val supparam_names = map fst supparams;
fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
val supexpr = (map (fn sup => (sup, (("", false),
- Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups,
+ (Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup)), [])))) sups,
map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams);
in (base_sort, supparam_names, supexpr, inferred_elems) end;
@@ -354,8 +354,8 @@
| NONE => error "Not in a class target");
val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
- val expr = ([(sup, (("", false), Expression.Positional []))], []);
- val (([props], deps, export), goal_ctxt) =
+ val expr = ([(sup, (("", false), (Expression.Positional [], [])))], []);
+ val (([props], _, deps, _, export), goal_ctxt) =
Expression.cert_goal_expression expr lthy;
val some_prop = try the_single props;
val some_dep_morph = try the_single (map snd deps);
--- a/src/Pure/Isar/expression.ML Tue Jan 16 15:53:42 2018 +0100
+++ b/src/Pure/Isar/expression.ML Tue Jan 16 19:28:05 2018 +0100
@@ -8,7 +8,7 @@
sig
(* Locale expressions *)
datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
- type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list
+ type ('name, 'term) expr = ('name * ((string * bool) * ('term map * (Attrib.binding * 'term) list))) list
type expression_i = (string, term) expr * (binding * typ option * mixfix) list
type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
@@ -38,9 +38,9 @@
(* Processing of locale expressions *)
val cert_goal_expression: expression_i -> Proof.context ->
- (term list list * (string * morphism) list * morphism) * Proof.context
+ (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
val read_goal_expression: expression -> Proof.context ->
- (term list list * (string * morphism) list * morphism) * Proof.context
+ (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
(* Diagnostic *)
val print_dependencies: Proof.context -> bool -> expression -> unit
@@ -58,7 +58,7 @@
Positional of 'term option list |
Named of (string * 'term) list;
-type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list;
+type ('name, 'term) expr = ('name * ((string * bool) * ('term map * (Attrib.binding * 'term) list))) list;
type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
@@ -92,7 +92,7 @@
Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2]));
fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
- fun params_inst (loc, (prfx, Positional insts)) =
+ fun params_inst (loc, (prfx, (Positional insts, eqns))) =
let
val ps = params_loc loc;
val d = length ps - length insts;
@@ -103,8 +103,8 @@
else insts @ replicate d NONE;
val ps' = (ps ~~ insts') |>
map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
- in (ps', (loc, (prfx, Positional insts'))) end
- | params_inst (loc, (prfx, Named insts)) =
+ in (ps', (loc, (prfx, (Positional insts', eqns)))) end
+ | params_inst (loc, (prfx, (Named insts, eqns))) =
let
val _ =
reject_dups "Duplicate instantiation of the following parameter(s): "
@@ -112,7 +112,7 @@
val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
if AList.defined (op =) ps p then AList.delete (op =) p ps
else error (quote p ^ " not a parameter of instantiated expression"));
- in (ps', (loc, (prfx, Named insts))) end;
+ in (ps', (loc, (prfx, (Named insts, eqns)))) end;
fun params_expr is =
let
val (is', ps') = fold_map (fn i => fn ps =>
@@ -232,6 +232,9 @@
fun extract_inst (_, (_, ts)) = map mk_term ts;
fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs));
+fun extract_eqns es = map (mk_term o snd) es;
+fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs;
+
fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes
| extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts
| extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms
@@ -266,17 +269,19 @@
in
-fun check_autofix insts elems concl ctxt =
+fun check_autofix insts eqnss elems concl ctxt =
let
val inst_cs = map extract_inst insts;
+ val eqns_cs = map extract_eqns eqnss;
val elem_css = map extract_elem elems;
val concl_cs = (map o map) mk_propp (map snd concl);
(* Type inference *)
- val (inst_cs' :: css', ctxt') =
- (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
+ val (inst_cs' :: eqns_cs' :: css', ctxt') =
+ (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt;
val (elem_css', [concl_cs']) = chop (length elem_css) css';
in
((map restore_inst (insts ~~ inst_cs'),
+ map restore_eqns (eqnss ~~ eqns_cs'),
map restore_elem (elems ~~ elem_css'),
map fst concl ~~ concl_cs'), ctxt')
end;
@@ -353,27 +358,32 @@
local
fun prep_full_context_statement
- parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_var_inst prep_expr
+ parse_typ parse_prop prep_obtains prep_var_elem prep_inst parse_eqn prep_var_inst prep_expr
{strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 =
let
val thy = Proof_Context.theory_of ctxt1;
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
- fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) =
+ fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
let
val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val inst' = prep_inst ctxt parm_names inst;
+ val eqns' = map (apsnd (parse_eqn ctxt)) eqns;
val parm_types' = parm_types
|> map (Type_Infer.paramify_vars o
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
val inst'' = map2 Type.constraint parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
- val ((insts'', _, _), _) = check_autofix insts' [] [] ctxt;
+ val eqnss' = eqnss @ [eqns'];
+ val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt;
val inst''' = insts'' |> List.last |> snd |> snd;
- val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
- val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
- in (i + 1, insts', ctxt'') end;
+ val eqns'' = eqnss'' |> List.last;
+ val (inst_morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
+ val rewrite_morph = eqns'' |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt) |>
+ Element.eq_morphism (Proof_Context.theory_of ctxt) |> the_default Morphism.identity;
+ val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
+ in (i + 1, insts', eqnss', ctxt'') end;
fun prep_elem raw_elem ctxt =
let
@@ -386,10 +396,10 @@
val fors = fold_map prep_var_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
- val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
+ val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2);
fun prep_stmt elems ctxt =
- check_autofix insts' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
+ check_autofix insts' eqnss' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
val _ =
if fixed_frees then ()
@@ -399,7 +409,7 @@
| frees => error ("Illegal free variables in expression: " ^
commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
- val ((insts, elems', concl), ctxt4) = ctxt3
+ val ((insts, eqnss, elems', concl), ctxt4) = ctxt3
|> init_body
|> fold_map prep_elem raw_elems
|-> prep_stmt;
@@ -416,21 +426,21 @@
val deps = map (finish_inst ctxt5) insts;
val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems';
- in ((fixed, deps, elems'', concl), (parms, ctxt5)) end;
+ in ((fixed, deps, eqnss, elems'', concl), (parms, ctxt5)) end;
in
fun cert_full_context_statement x =
prep_full_context_statement (K I) (K I) Obtain.cert_obtains
- Proof_Context.cert_var make_inst Proof_Context.cert_var (K I) x;
+ Proof_Context.cert_var make_inst (K I) Proof_Context.cert_var (K I) x;
fun cert_read_full_context_statement x =
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
- Proof_Context.read_var make_inst Proof_Context.cert_var (K I) x;
+ Proof_Context.read_var make_inst (K I) Proof_Context.cert_var (K I) x;
fun read_full_context_statement x =
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
- Proof_Context.read_var parse_inst Proof_Context.read_var check_expr x;
+ Proof_Context.read_var parse_inst (Syntax.parse_prop) Proof_Context.read_var check_expr x;
end;
@@ -441,7 +451,7 @@
fun prep_statement prep activate raw_elems raw_stmt ctxt =
let
- val ((_, _, elems, concl), _) =
+ val ((_, _, _, elems, concl), _) =
prep {strict = true, do_close = false, fixed_frees = true}
([], []) I raw_elems raw_stmt ctxt;
val ctxt' = ctxt
@@ -467,9 +477,10 @@
fun prep_declaration prep activate raw_import init_body raw_elems ctxt =
let
- val ((fixed, deps, elems, _), (parms, ctxt0)) =
+ val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) =
prep {strict = false, do_close = true, fixed_frees = false}
raw_import init_body raw_elems (Element.Shows []) ctxt;
+ val _ = null (flat eqnss) orelse error "Illegal replaces clause(s) in declaration of locale";
(* Declare parameters and imported facts *)
val ctxt' = ctxt
|> fix_params fixed
@@ -505,11 +516,12 @@
let
val thy = Proof_Context.theory_of ctxt;
- val ((fixed, deps, _, _), _) =
+ val ((fixed, deps, eqnss, _, _), _) =
prep {strict = true, do_close = true, fixed_frees = true} expression I []
(Element.Shows []) ctxt;
(* proof obligations *)
val propss = map (props_of thy) deps;
+ val eq_propss = (map o map) snd eqnss;
val goal_ctxt = ctxt
|> fix_params fixed
@@ -522,7 +534,7 @@
val export' =
Morphism.morphism "Expression.prep_goal"
{binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
- in ((propss, deps, export'), goal_ctxt) end;
+ in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end;
in
@@ -844,7 +856,7 @@
fun print_dependencies ctxt clean expression =
let
- val ((_, deps, export), expr_ctxt) = read_goal_expression expression ctxt;
+ val ((_, _, deps, _, export), expr_ctxt) = read_goal_expression expression ctxt;
val export' = if clean then Morphism.identity else export;
in
Locale.print_dependencies expr_ctxt clean export' deps
--- a/src/Pure/Isar/interpretation.ML Tue Jan 16 15:53:42 2018 +0100
+++ b/src/Pure/Isar/interpretation.ML Tue Jan 16 19:28:05 2018 +0100
@@ -55,7 +55,7 @@
local
-fun augment_with_def prep_term deps ((name, atts), ((b, mx), raw_rhs)) lthy =
+fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy =
let
val rhs = prep_term lthy raw_rhs;
val lthy' = Variable.declare_term rhs lthy;
@@ -63,7 +63,7 @@
Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
in (def, lthy'') end;
-fun augment_with_defs prep_term [] deps ctxt = ([], ctxt)
+fun augment_with_defs _ [] _ ctxt = ([], ctxt)
(*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
| augment_with_defs prep_term raw_defs deps lthy =
let
@@ -71,7 +71,7 @@
Local_Theory.open_target lthy
||> fold Locale.activate_declarations deps;
val (inner_defs, inner_lthy') =
- fold_map (augment_with_def prep_term deps) raw_defs inner_lthy;
+ fold_map (augment_with_def prep_term) raw_defs inner_lthy;
val lthy' =
inner_lthy'
|> Local_Theory.close_target;
@@ -79,9 +79,11 @@
map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
in (def_eqns, lthy') end;
-fun prep_eqns prep_props prep_attr [] deps ctxt = ([], [])
+fun prep_eqns _ _ [] _ _ = ([], [])
| prep_eqns prep_props prep_attr raw_eqns deps ctxt =
let
+ (* FIXME incompatibility, creating context for parsing rewrites equation may fail in
+ presence of replaces clause *)
val ctxt' = fold Locale.activate_declarations deps ctxt;
val eqns =
(Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns;
@@ -91,13 +93,13 @@
fun prep_interpretation prep_expr prep_term prep_props prep_attr
expression raw_defs raw_eqns initial_ctxt =
let
- val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
+ val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
val (def_eqns, def_ctxt) =
augment_with_defs prep_term raw_defs deps expr_ctxt;
val (eqns, attrss) = prep_eqns prep_props prep_attr raw_eqns deps def_ctxt;
val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
+ in (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
in
@@ -119,13 +121,17 @@
fun meta_rewrite eqns ctxt =
(map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
-fun note_eqns_register pos note activate deps witss def_eqns eqns attrss export export' ctxt =
+fun note_eqns_register pos note activate deps eqnss witss def_eqns thms attrss export export' ctxt =
let
+ val (thmss, thms') = split_last (unflat ((map o map) fst eqnss @ [attrss]) thms);
+ val factss =
+ map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss;
+ val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt;
val facts =
(Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) ::
map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])]))
- attrss eqns;
- val (eqns', ctxt') = ctxt
+ attrss thms';
+ val (eqns', ctxt'') = ctxt'
|> note Thm.theoremK facts
|-> meta_rewrite;
val dep_morphs =
@@ -134,23 +140,23 @@
$> Element.satisfy_morphism (map (Element.transform_witness export') wits)
$> Morphism.binding_morphism "position" (Binding.set_pos pos)
in (dep, morph') end) deps witss;
- fun activate' dep_morph ctxt =
+ fun activate' (dep_morph, eqns) ctxt =
activate dep_morph
- (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
+ (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')))
export ctxt;
- in ctxt' |> fold activate' dep_morphs end;
+ in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end;
in
fun generic_interpretation prep_interpretation setup_proof note add_registration
expression raw_defs raw_eqns initial_ctxt =
let
- val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
+ val (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
prep_interpretation expression raw_defs raw_eqns initial_ctxt;
val pos = Position.thread_data ();
fun after_qed witss eqns =
- note_eqns_register pos note add_registration deps witss def_eqns eqns attrss export export';
- in setup_proof after_qed propss eqns goal_ctxt end;
+ note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns attrss export export';
+ in setup_proof after_qed propss (flat (eq_propss @ [eqns])) goal_ctxt end;
end;
--- a/src/Pure/Isar/parse_spec.ML Tue Jan 16 15:53:42 2018 +0100
+++ b/src/Pure/Isar/parse_spec.ML Tue Jan 16 19:28:05 2018 +0100
@@ -111,9 +111,10 @@
fun plus1_unless test scan =
scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
-val instance = Parse.where_ |--
+val instance = Scan.optional (Parse.where_ |--
Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
- Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
+ Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional) (Expression.Named []) --
+ (Scan.optional (Parse.$$$ "replaces" |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []);
in
@@ -133,7 +134,7 @@
val expr2 = Parse.position Parse.name;
val expr1 =
locale_prefix -- expr2 --
- Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
+ instance >> (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/Pure.thy Tue Jan 16 15:53:42 2018 +0100
+++ b/src/Pure/Pure.thy Tue Jan 16 19:28:05 2018 +0100
@@ -10,7 +10,7 @@
"\<subseteq>" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
"overloaded" "pervasive" "premises" "structure" "unchecked"
and "private" "qualified" :: before_command
- and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
+ and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "replaces" "rewrites"
"obtains" "shows" "when" "where" "|" :: quasi_command
and "text" "txt" :: document_body
and "text_raw" :: document_raw