--- 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
--- 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"
--- /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
--- 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,
--- 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
--- 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
--- 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
--- 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
--- 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