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.
proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory";
authorwenzelm
Sat, 30 Nov 2019 16:46:34 +0100
changeset 71205 95e12ecdcb5f
parent 71204 abb0d984abbc
child 71206 20dce31fe7f4
proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory";
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Nov 30 16:42:15 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Nov 30 16:46:34 2019 +0100
@@ -2154,10 +2154,10 @@
       in
         lthy11
 (* TODO:
-        |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat sel_thmss)
-        |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat ctr_thmss)
+        |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat sel_thmss)
+        |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat ctr_thmss)
 *)
-        |> Spec_Rules.add "" Spec_Rules.equational [fun_lhs0] [code_thm]
+        |> Spec_Rules.add "" Spec_Rules.equational [fun_lhs] [code_thm]
         |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
         |> Local_Theory.notes (anonymous_notes @ notes)
         |> snd
isabelle