src/HOL/Ctr_Sugar.thy
changeset 54701 4ed7454aebde
parent 54626 8a5e82425e55
child 55160 2d69438b1b0c
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Mon Dec 09 06:33:46 2013 +0100
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Mon Dec 09 09:44:57 2013 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  declare [[coercion_args case_abs -]]
     1.5  declare [[coercion_args case_elem - +]]
     1.6  
     1.7 -ML_file "Tools/case_translation.ML"
     1.8 +ML_file "Tools/Ctr_Sugar/case_translation.ML"
     1.9  setup Case_Translation.setup
    1.10  
    1.11  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    1.12 @@ -36,9 +36,9 @@
    1.13  "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    1.14  by blast+
    1.15  
    1.16 -ML_file "Tools/ctr_sugar_util.ML"
    1.17 -ML_file "Tools/ctr_sugar_tactics.ML"
    1.18 -ML_file "Tools/ctr_sugar_code.ML"
    1.19 -ML_file "Tools/ctr_sugar.ML"
    1.20 +ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
    1.21 +ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
    1.22 +ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
    1.23 +ML_file "Tools/Ctr_Sugar/ctr_sugar.ML"
    1.24  
    1.25  end