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