# HG changeset patch
# User berghofe
# Date 1222117215 -7200
# Node ID 0b6b83ec845862042a96a618c4d877caf2e971a7
# Parent  0dd1a0b16a375ea419c31cf755b3561049b8bbbb
Added setup for coherent logic prover.

diff -r 0dd1a0b16a37 -r 0b6b83ec8458 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Sep 22 22:59:35 2008 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 22 23:00:15 2008 +0200
@@ -19,6 +19,7 @@
   "~~/src/Provers/classical.ML"
   "~~/src/Provers/blast.ML"
   "~~/src/Provers/clasimp.ML"
+  "~~/src/Provers/coherent.ML"
   "~~/src/Provers/eqsubst.ML"
   "~~/src/Provers/quantifier1.ML"
   ("simpdata.ML")
@@ -1563,6 +1564,23 @@
 setup InductTacs.setup
 
 
+subsubsection {* Coherent logic *}
+
+ML {*
+structure Coherent = CoherentFun
+(
+  val atomize_elimL = @{thm atomize_elimL}
+  val atomize_exL = @{thm atomize_exL}
+  val atomize_conjL = @{thm atomize_conjL}
+  val atomize_disjL = @{thm atomize_disjL}
+  val operator_names =
+    [@{const_name "op |"}, @{const_name "op &"}, @{const_name "Ex"}]
+);
+*}
+
+setup Coherent.setup
+
+
 subsection {* Other simple lemmas and lemma duplicates *}
 
 lemma Let_0 [simp]: "Let 0 f = f 0"