equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Wrapping Existing Freely Generated Type's Constructors *} |
8 header {* Wrapping Existing Freely Generated Type's Constructors *} |
9 |
9 |
10 theory Ctr_Sugar |
10 theory Ctr_Sugar |
11 imports BNF_Util |
11 imports Main |
12 keywords |
12 keywords |
13 "wrap_free_constructors" :: thy_goal and |
13 "wrap_free_constructors" :: thy_goal and |
14 "no_discs_sels" and |
14 "no_discs_sels" and |
15 "rep_compat" |
15 "rep_compat" |
16 begin |
16 begin |
21 lemma iff_contradict: |
21 lemma iff_contradict: |
22 "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R" |
22 "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R" |
23 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R" |
23 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R" |
24 by blast+ |
24 by blast+ |
25 |
25 |
|
26 ML_file "Tools/ctr_sugar_util.ML" |
26 ML_file "Tools/ctr_sugar_tactics.ML" |
27 ML_file "Tools/ctr_sugar_tactics.ML" |
27 ML_file "Tools/ctr_sugar.ML" |
28 ML_file "Tools/ctr_sugar.ML" |
28 |
29 |
29 end |
30 end |