src/HOL/HOL.thy
changeset 55632 0f9d03649a9c
parent 55385 169e12bbf9a3
child 55757 9fc71814b8c1
     1.1 --- a/src/HOL/HOL.thy	Thu Feb 20 19:55:39 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Feb 20 20:19:41 2014 +0100
     1.3 @@ -24,7 +24,6 @@
     1.4  ML_file "~~/src/Provers/classical.ML"
     1.5  ML_file "~~/src/Provers/blast.ML"
     1.6  ML_file "~~/src/Provers/clasimp.ML"
     1.7 -ML_file "~~/src/Tools/coherent.ML"
     1.8  ML_file "~~/src/Tools/eqsubst.ML"
     1.9  ML_file "~~/src/Provers/quantifier1.ML"
    1.10  ML_file "~~/src/Tools/atomize_elim.ML"
    1.11 @@ -1561,20 +1560,18 @@
    1.12  
    1.13  subsubsection {* Coherent logic *}
    1.14  
    1.15 +ML_file "~~/src/Tools/coherent.ML"
    1.16  ML {*
    1.17  structure Coherent = Coherent
    1.18  (
    1.19 -  val atomize_elimL = @{thm atomize_elimL}
    1.20 -  val atomize_exL = @{thm atomize_exL}
    1.21 -  val atomize_conjL = @{thm atomize_conjL}
    1.22 -  val atomize_disjL = @{thm atomize_disjL}
    1.23 -  val operator_names =
    1.24 -    [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
    1.25 +  val atomize_elimL = @{thm atomize_elimL};
    1.26 +  val atomize_exL = @{thm atomize_exL};
    1.27 +  val atomize_conjL = @{thm atomize_conjL};
    1.28 +  val atomize_disjL = @{thm atomize_disjL};
    1.29 +  val operator_names = [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}];
    1.30  );
    1.31  *}
    1.32  
    1.33 -setup Coherent.setup
    1.34 -
    1.35  
    1.36  subsubsection {* Reorienting equalities *}
    1.37