# HG changeset patch
# User blanchet
# Date 1380629125 -7200
# Node ID 9fe1bd54d4378eaad72c45e56aff616df7594956
# Parent  132640f4c4534f887986ae08d6c204fd7b073051
renamed theory file

diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/BNF_Ctr_Sugar.thy
--- a/src/HOL/BNF/BNF_Ctr_Sugar.thy	Tue Oct 01 12:53:24 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(*  Title:      HOL/BNF/BNF_Ctr_Sugar.thy
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012
-
-Wrapping existing freely generated type's constructors.
-*)
-
-header {* Wrapping Existing Freely Generated Type's Constructors *}
-
-theory BNF_Ctr_Sugar
-imports BNF_Util
-keywords
-  "wrap_free_constructors" :: thy_goal and
-  "no_discs_sels" and
-  "rep_compat"
-begin
-
-lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
-by (erule iffI) (erule contrapos_pn)
-
-lemma iff_contradict:
-"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
-"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
-by blast+
-
-ML_file "Tools/bnf_ctr_sugar_tactics.ML"
-ML_file "Tools/bnf_ctr_sugar.ML"
-
-end
diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/BNF_FP_Base.thy
--- a/src/HOL/BNF/BNF_FP_Base.thy	Tue Oct 01 12:53:24 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Tue Oct 01 14:05:25 2013 +0200
@@ -10,7 +10,7 @@
 header {* Shared Fixed Point Operations on Bounded Natural Functors *}
 
 theory BNF_FP_Base
-imports BNF_Comp BNF_Ctr_Sugar
+imports BNF_Comp Ctr_Sugar
 begin
 
 lemma not_TrueE: "\<not> True \<Longrightarrow> P"
diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Ctr_Sugar.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Ctr_Sugar.thy	Tue Oct 01 14:05:25 2013 +0200
@@ -0,0 +1,29 @@
+(*  Title:      HOL/BNF/Ctr_Sugar.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Wrapping existing freely generated type's constructors.
+*)
+
+header {* Wrapping Existing Freely Generated Type's Constructors *}
+
+theory Ctr_Sugar
+imports BNF_Util
+keywords
+  "wrap_free_constructors" :: thy_goal and
+  "no_discs_sels" and
+  "rep_compat"
+begin
+
+lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
+by (erule iffI) (erule contrapos_pn)
+
+lemma iff_contradict:
+"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
+"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
+by blast+
+
+ML_file "Tools/bnf_ctr_sugar_tactics.ML"
+ML_file "Tools/bnf_ctr_sugar.ML"
+
+end
diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Oct 01 12:53:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
@@ -5,7 +5,7 @@
 Wrapping existing freely generated type's constructors.
 *)
 
-signature BNF_CTR_SUGAR =
+signature CTR_SUGAR =
 sig
   type ctr_sugar =
     {ctrs: term list,
@@ -57,11 +57,11 @@
   val parse_bound_term: (binding * string) parser
 end;
 
-structure BNF_Ctr_Sugar : BNF_CTR_SUGAR =
+structure Ctr_Sugar : CTR_SUGAR =
 struct
 
 open BNF_Util
-open BNF_Ctr_Sugar_Tactics
+open Ctr_Sugar_Tactics
 
 type ctr_sugar =
   {ctrs: term list,
diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Tue Oct 01 12:53:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Tue Oct 01 14:05:25 2013 +0200
@@ -5,7 +5,7 @@
 Tactics for wrapping existing freely generated type's constructors.
 *)
 
-signature BNF_CTR_SUGAR_TACTICS =
+signature CTR_SUGAR_TACTICS =
 sig
   val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
   val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
@@ -26,7 +26,7 @@
   val mk_unique_disc_def_tac: int -> thm -> tactic
 end;
 
-structure BNF_Ctr_Sugar_Tactics : BNF_CTR_SUGAR_TACTICS =
+structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
 struct
 
 open BNF_Util
diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 01 12:53:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
@@ -16,7 +16,7 @@
      nesting_bnfs: BNF_Def.bnf list,
      fp_res: BNF_FP_Util.fp_result,
      ctr_defss: thm list list,
-     ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
+     ctr_sugars: Ctr_Sugar.ctr_sugar list,
      co_iterss: term list list,
      mapss: thm list list,
      co_inducts: thm list,
@@ -87,7 +87,7 @@
     string * term list * term list list * ((term list list * term list list list)
       * (typ list * typ list list)) list ->
     thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
-    int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list ->
+    int list list -> int list list -> int list -> thm list list -> Ctr_Sugar.ctr_sugar list ->
     term list list -> thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
   val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
@@ -105,8 +105,8 @@
 structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR =
 struct
 
+open Ctr_Sugar
 open BNF_Util
-open BNF_Ctr_Sugar
 open BNF_Comp
 open BNF_Def
 open BNF_FP_Util
diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 12:53:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Oct 01 14:05:25 2013 +0200
@@ -25,9 +25,9 @@
 structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
 struct
 
+open Ctr_Sugar
 open BNF_Util
 open BNF_Def
-open BNF_Ctr_Sugar
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M
diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Oct 01 12:53:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Oct 01 14:05:25 2013 +0200
@@ -83,9 +83,9 @@
 structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
 struct
 
+open Ctr_Sugar
 open BNF_Util
 open BNF_Def
-open BNF_Ctr_Sugar
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M_Sugar
diff -r 132640f4c453 -r 9fe1bd54d437 src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Oct 01 12:53:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Oct 01 14:05:25 2013 +0200
@@ -13,8 +13,8 @@
 structure BNF_LFP_Compat : BNF_LFP_COMPAT =
 struct
 
+open Ctr_Sugar
 open BNF_Util
-open BNF_Ctr_Sugar
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M_Sugar