| changeset 58177 | 166131276380 |
| parent 57631 | 959caab43a3d |
| child 58188 | cc71d2be4f0a |
--- a/src/HOL/Ctr_Sugar.thy Wed Sep 03 22:47:48 2014 +0200 +++ b/src/HOL/Ctr_Sugar.thy Wed Sep 03 22:49:05 2014 +0200 @@ -37,6 +37,7 @@ "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R" by blast+ +ML_file "Tools/Ctr_Sugar/local_interpretation.ML" ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML" ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML" ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"