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.
compile
authorblanchet
Thu, 11 Sep 2014 19:41:45 +0200
changeset 58314 ee1be8b3032e
parent 58313 57d2e5006d29
child 58315 6d8458bc6e27
compile
src/HOL/BNF_Least_Fixpoint.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/BNF/bnf_lfp.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 11 19:39:48 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 11 19:41:45 2014 +0200
@@ -13,7 +13,6 @@
 imports BNF_Fixpoint_Base
 keywords
   "datatype" :: thy_decl and
-  "datatype" :: thy_decl and
   "datatype_compat" :: thy_decl
 begin
 
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 19:39:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 19:41:45 2014 +0200
@@ -1817,10 +1817,6 @@
   Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
     (parse_co_datatype_cmd Least_FP construct_lfp);
 
-val _ =
-  Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
-    (parse_co_datatype_cmd Least_FP construct_lfp);
-
 val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
 
 end;
isabelle