src/HOL/HOL.thy
changeset 28325 0b6b83ec8458
parent 28227 77221ee0f7b9
child 28346 b8390cd56b8f
     1.1 --- a/src/HOL/HOL.thy	Mon Sep 22 22:59:35 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 22 23:00:15 2008 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    "~~/src/Provers/classical.ML"
     1.5    "~~/src/Provers/blast.ML"
     1.6    "~~/src/Provers/clasimp.ML"
     1.7 +  "~~/src/Provers/coherent.ML"
     1.8    "~~/src/Provers/eqsubst.ML"
     1.9    "~~/src/Provers/quantifier1.ML"
    1.10    ("simpdata.ML")
    1.11 @@ -1563,6 +1564,23 @@
    1.12  setup InductTacs.setup
    1.13  
    1.14  
    1.15 +subsubsection {* Coherent logic *}
    1.16 +
    1.17 +ML {*
    1.18 +structure Coherent = CoherentFun
    1.19 +(
    1.20 +  val atomize_elimL = @{thm atomize_elimL}
    1.21 +  val atomize_exL = @{thm atomize_exL}
    1.22 +  val atomize_conjL = @{thm atomize_conjL}
    1.23 +  val atomize_disjL = @{thm atomize_disjL}
    1.24 +  val operator_names =
    1.25 +    [@{const_name "op |"}, @{const_name "op &"}, @{const_name "Ex"}]
    1.26 +);
    1.27 +*}
    1.28 +
    1.29 +setup Coherent.setup
    1.30 +
    1.31 +
    1.32  subsection {* Other simple lemmas and lemma duplicates *}
    1.33  
    1.34  lemma Let_0 [simp]: "Let 0 f = f 0"