--- a/src/HOL/IMP/Abs_Int1_const.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Feb 19 22:05:15 2014 +0100
@@ -69,7 +69,7 @@
permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defines AI_const is AI and step_const is step' and aval'_const is aval'
+defining AI_const = AI and step_const = step' and aval'_const = aval'
..
--- a/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 19 22:05:15 2014 +0100
@@ -125,7 +125,7 @@
permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-defines aval_parity is aval' and step_parity is step' and AI_parity is AI
+defining aval_parity = aval' and step_parity = step' and AI_parity = AI
..
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed Feb 19 22:05:15 2014 +0100
@@ -320,7 +320,7 @@
permanent_interpretation Val_lattice_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
-defines aval_ivl is aval'
+defining aval_ivl = aval'
proof
case goal1 show ?case by(simp add: \<gamma>_inf)
next
@@ -354,11 +354,11 @@
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
-defines inv_aval_ivl is inv_aval'
-and inv_bval_ivl is inv_bval'
-and step_ivl is step'
-and AI_ivl is AI
-and aval_ivl' is aval''
+defining inv_aval_ivl = inv_aval'
+and inv_bval_ivl = inv_bval'
+and step_ivl = step'
+and AI_ivl = AI
+and aval_ivl' = aval''
..
--- a/src/HOL/IMP/Abs_Int3.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Wed Feb 19 22:05:15 2014 +0100
@@ -264,7 +264,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
-defines AI_wn_ivl is AI_wn
+defining AI_wn_ivl = AI_wn
..
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Wed Feb 19 22:05:15 2014 +0100
@@ -62,8 +62,8 @@
qed
permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
-defines AI_const is AI
-and aval'_const is aval'
+defining AI_const = AI
+and aval'_const = aval'
proof qed (auto simp: iter'_pfp_above)
text{* Straight line code: *}
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Wed Feb 19 22:05:15 2014 +0100
@@ -202,10 +202,10 @@
permanent_interpretation
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
-defines afilter_ivl is afilter
-and bfilter_ivl is bfilter
-and AI_ivl is AI
-and aval_ivl is aval'
+defining afilter_ivl = afilter
+and bfilter_ivl = bfilter
+and AI_ivl = AI
+and aval_ivl = aval'
proof qed (auto simp: iter'_pfp_above)
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Feb 19 22:05:15 2014 +0100
@@ -194,10 +194,10 @@
permanent_interpretation
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
-defines afilter_ivl' is afilter
-and bfilter_ivl' is bfilter
-and AI_ivl' is AI
-and aval_ivl' is aval'
+defining afilter_ivl' = afilter
+and bfilter_ivl' = bfilter
+and AI_ivl' = AI
+and aval_ivl' = aval'
proof qed (auto simp: iter'_pfp_above)
value [code] "list_up(AI_ivl' test3_ivl Top)"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Wed Feb 19 22:05:15 2014 +0100
@@ -68,7 +68,7 @@
permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defines AI_const is AI and step_const is step' and aval'_const is aval'
+defining AI_const = AI and step_const = step' and aval'_const = aval'
..
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Wed Feb 19 22:05:15 2014 +0100
@@ -115,7 +115,7 @@
permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-defines aval_parity is aval' and step_parity is step' and AI_parity is AI
+defining aval_parity = aval' and step_parity = step' and AI_parity = AI
..
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Wed Feb 19 22:05:15 2014 +0100
@@ -181,7 +181,7 @@
permanent_interpretation Val_abs1_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
-defines aval_ivl is aval'
+defining 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,11 +219,11 @@
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
-defines afilter_ivl is afilter
-and bfilter_ivl is bfilter
-and step_ivl is step'
-and AI_ivl is AI
-and aval_ivl' is aval''
+defining afilter_ivl = afilter
+and bfilter_ivl = bfilter
+and step_ivl = step'
+and AI_ivl = AI
+and aval_ivl' = aval''
..
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Wed Feb 19 22:05:15 2014 +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
-defines AI_ivl' is AI_wn
+defining AI_ivl' = AI_wn
..
--- a/src/HOL/ex/Interpretation_with_Defs.thy Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/ex/Interpretation_with_Defs.thy Wed Feb 19 22:05:15 2014 +0100
@@ -6,7 +6,7 @@
theory Interpretation_with_Defs
imports Pure
-keywords "permanent_interpretation" :: thy_goal
+keywords "defining" and "permanent_interpretation" :: thy_goal
begin
ML_file "~~/src/Tools/interpretation_with_defs.ML"
--- a/src/Tools/interpretation_with_defs.ML Wed Feb 19 22:05:05 2014 +0100
+++ b/src/Tools/interpretation_with_defs.ML Wed Feb 19 22:05:15 2014 +0100
@@ -102,8 +102,8 @@
Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
"prove interpretation of locale expression into named theory"
(Parse.!!! (Parse_Spec.locale_expression true) --
- Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
- -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
+ Scan.optional (@{keyword "defining"} |-- 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)) []
>> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));