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"
```