--- a/src/Doc/Codegen/Further.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Doc/Codegen/Further.thy Sat Nov 14 08:45:52 2015 +0100
@@ -229,7 +229,7 @@
(*>*)
permanent_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"
- defining funpows = "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+ defines funpows = "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
by unfold_locales
(simp_all add: fun_eq_iff funpow_mult mult.commute) (*<*)
--- a/src/Doc/Isar_Ref/Spec.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Nov 14 08:45:52 2015 +0100
@@ -756,12 +756,12 @@
@@{command permanent_interpretation} @{syntax locale_expr} \<newline>
definitions? equations?
;
- definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline>
+ definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
@{syntax mixfix}? @'=' @{syntax term} + @'and');
equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \<^descr> \<^theory_text>\<open>permanent_interpretation expr defining "defs" rewrites eqns\<close> interprets
+ \<^descr> \<^theory_text>\<open>permanent_interpretation expr defines "defs" rewrites eqns\<close> interprets
\<open>expr\<close> in the current local theory. The command generates proof obligations
for the instantiated specifications. Instantiated declarations (in
particular, facts) are added to the local theory's underlying target in a
--- a/src/Doc/isar.sty Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Doc/isar.sty Sat Nov 14 08:45:52 2015 +0100
@@ -18,7 +18,6 @@
\newcommand{\isasymAND}{\isakeyword{and}}
\newcommand{\isasymIS}{\isakeyword{is}}
\newcommand{\isasymWHERE}{\isakeyword{where}}
-\newcommand{\isasymDEFINING}{\isakeyword{defining}}
\newcommand{\isasymBEGIN}{\isakeyword{begin}}
\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
\newcommand{\isasymIN}{\isakeyword{in}}
--- a/src/HOL/IMP/Abs_Int1_const.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Sat Nov 14 08:45:52 2015 +0100
@@ -68,7 +68,7 @@
permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defining AI_const = AI and step_const = step' and aval'_const = aval'
+defines AI_const = AI and step_const = step' and aval'_const = aval'
..
--- a/src/HOL/IMP/Abs_Int1_parity.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Sat Nov 14 08:45:52 2015 +0100
@@ -126,7 +126,7 @@
permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-defining aval_parity = aval' and step_parity = step' and AI_parity = AI
+defines aval_parity = aval' and step_parity = step' and AI_parity = AI
..
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Sat Nov 14 08:45:52 2015 +0100
@@ -320,7 +320,7 @@
permanent_interpretation Val_lattice_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
-defining aval_ivl = aval'
+defines aval_ivl = aval'
proof (standard, goal_cases)
case 1 show ?case by(simp add: \<gamma>_inf)
next
@@ -354,7 +354,7 @@
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
-defining inv_aval_ivl = inv_aval'
+defines inv_aval_ivl = inv_aval'
and inv_bval_ivl = inv_bval'
and step_ivl = step'
and AI_ivl = AI
--- a/src/HOL/IMP/Abs_Int3.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Sat Nov 14 08:45:52 2015 +0100
@@ -260,7 +260,7 @@
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
-defining AI_wn_ivl = AI_wn
+defines AI_wn_ivl = AI_wn
..
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Sat Nov 14 08:45:52 2015 +0100
@@ -62,7 +62,7 @@
qed
permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
-defining AI_const = AI
+defines AI_const = AI
and aval'_const = aval'
proof qed (auto simp: iter'_pfp_above)
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sat Nov 14 08:45:52 2015 +0100
@@ -202,7 +202,7 @@
permanent_interpretation
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
-defining afilter_ivl = afilter
+defines afilter_ivl = afilter
and bfilter_ivl = bfilter
and AI_ivl = AI
and aval_ivl = aval'
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Sat Nov 14 08:45:52 2015 +0100
@@ -194,7 +194,7 @@
permanent_interpretation
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
-defining afilter_ivl' = afilter
+defines afilter_ivl' = afilter
and bfilter_ivl' = bfilter
and AI_ivl' = AI
and aval_ivl' = aval'
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Sat Nov 14 08:45:52 2015 +0100
@@ -68,7 +68,7 @@
permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defining AI_const = AI and step_const = step' and aval'_const = aval'
+defines AI_const = AI and step_const = step' and aval'_const = aval'
..
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Sat Nov 14 08:45:52 2015 +0100
@@ -115,7 +115,7 @@
permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-defining aval_parity = aval' and step_parity = step' and AI_parity = AI
+defines aval_parity = aval' and step_parity = step' and AI_parity = AI
..
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Sat Nov 14 08:45:52 2015 +0100
@@ -181,7 +181,7 @@
permanent_interpretation Val_abs1_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
-defining aval_ivl = aval'
+defines aval_ivl = aval'
proof
case goal1 thus ?case
by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -219,7 +219,7 @@
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
-defining afilter_ivl = afilter
+defines afilter_ivl = afilter
and bfilter_ivl = bfilter
and step_ivl = step'
and AI_ivl = AI
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Sat Nov 14 08:45:52 2015 +0100
@@ -229,7 +229,7 @@
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
-defining AI_ivl' = AI_wn
+defines AI_ivl' = AI_wn
..
--- a/src/HOL/Library/Groups_Big_Fun.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sat Nov 14 08:45:52 2015 +0100
@@ -225,7 +225,7 @@
"Sum_any = comm_monoid_fun.G plus 0"
permanent_interpretation Sum_any: comm_monoid_fun plus 0
-where
+rewrites
"comm_monoid_fun.G plus 0 = Sum_any" and
"comm_monoid_set.F plus 0 = setsum"
proof -
@@ -298,7 +298,7 @@
"Prod_any = comm_monoid_fun.G times 1"
permanent_interpretation Prod_any: comm_monoid_fun times 1
-where
+rewrites
"comm_monoid_fun.G times 1 = Prod_any" and
"comm_monoid_set.F times 1 = setprod"
proof -
--- a/src/Pure/Isar/isar_syn.ML Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Nov 14 08:45:52 2015 +0100
@@ -419,10 +419,10 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
"prove interpretation of locale expression into named theory"
- (Parse.!!! (Parse_Spec.locale_expression true) --
- Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+ (Parse.!!! Parse_Spec.locale_expression --
+ Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
- Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
+ Scan.optional (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
>> (fn ((expr, defs), eqns) => Interpretation.permanent_interpretation_cmd expr defs eqns));
val _ =
--- a/src/Pure/Pure.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Pure/Pure.thy Sat Nov 14 08:45:52 2015 +0100
@@ -9,7 +9,7 @@
"!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
"\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
- "defines" "defining" "fixes" "for" "identifier" "if" "in" "includes" "infix"
+ "defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
"shows" "structure" "unchecked" "where" "when" "|"