Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature
authortraytel
Tue, 23 Aug 2016 15:19:32 +0200
changeset 63719 9084d77f1119
parent 63718 600cf5c8f2ba
child 63720 bcf2123d059a
tuned signature
src/HOL/Tools/BNF/bnf_gfp_grec.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/BNF/bnf_lfp_compat.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Fri Aug 19 11:56:12 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Aug 23 15:19:32 2016 +0200
@@ -265,7 +265,7 @@
     val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
       |> Local_Theory.open_target |> snd
       |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
-      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
+      |> primrec [] [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Aug 19 11:56:12 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Aug 23 15:19:32 2016 +0200
@@ -82,6 +82,9 @@
   val gfp_rec_sugar_interpretation: string ->
     (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
+  val primcorec_ursive: bool -> corec_option list -> ((binding * typ) * mixfix) list ->
+    ((binding * Token.T list list) * term) list -> term option list ->  Proof.context ->
+    (term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory
   val primcorec_ursive_cmd: bool -> corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     Proof.context ->
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Aug 19 11:56:12 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Aug 23 15:19:32 2016 +0200
@@ -535,9 +535,9 @@
 
 fun old_of_new f (ts, _, simpss) = (ts, f simpss);
 
-val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec;
-val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global;
-val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded;
+val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec [];
+val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global [];
+val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded [];
 val primrec_simple = apfst (apfst fst o apsnd (old_of_new (flat o snd))) ooo
   BNF_LFP_Rec_Sugar.primrec_simple;
 
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Aug 19 11:56:12 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Aug 23 15:19:32 2016 +0200
@@ -62,17 +62,19 @@
   val lfp_rec_sugar_interpretation: string ->
     (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
-  val primrec: (binding * typ option * mixfix) list -> Specification.multi_specs ->
-    local_theory -> (term list * thm list * thm list list) * local_theory
+  val primrec: rec_option list -> (binding * typ option * mixfix) list ->
+    Specification.multi_specs -> local_theory ->
+    (term list * thm list * thm list list) * local_theory
   val primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
     Specification.multi_specs_cmd -> local_theory ->
     (term list * thm list * thm list list) * local_theory
-  val primrec_global: (binding * typ option * mixfix) list ->
+  val primrec_global: rec_option list -> (binding * typ option * mixfix) list ->
     Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
-  val primrec_overloaded: (string * (string * typ) * bool) list ->
+  val primrec_overloaded: rec_option list -> (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
     Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
-  val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory ->
+  val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
+    local_theory ->
     ((string list * (binding -> binding) list) *
     (term list * thm list * (int list list * thm list list))) * local_theory
 end;
@@ -666,17 +668,17 @@
     old_primrec raw_fixes raw_specs lthy
     |>> (fn (ts, thms) => (ts, [], [thms]));
 
-val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs [];
+val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs;
 val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs;
 
-fun primrec_global fixes specs =
+fun primrec_global opts fixes specs =
   Named_Target.theory_init
-  #> primrec fixes specs
+  #> primrec opts fixes specs
   ##> Local_Theory.exit_global;
 
-fun primrec_overloaded ops fixes specs =
+fun primrec_overloaded opts ops fixes specs =
   Overloading.overloading ops
-  #> primrec fixes specs
+  #> primrec opts fixes specs
   ##> Local_Theory.exit_global;
 
 val rec_option_parser = Parse.group (K "option")
isabelle