src/HOL/HOL.thy
 changeset 14201 7ad7ab89c402 parent 13764 3e180bf68496 child 14208 144f45277d5a
```--- a/src/HOL/HOL.thy	Tue Sep 23 15:41:33 2003 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 23 15:42:01 2003 +0200
@@ -380,6 +380,18 @@
-- {* Miniscoping: pushing in universal quantifiers. *}
by (rules | blast)+

+lemma disj_absorb: "(A | A) = A"
+  by blast
+
+lemma disj_left_absorb: "(A | (A | B)) = (A | B)"
+  by blast
+
+lemma conj_absorb: "(A & A) = A"
+  by blast
+
+lemma conj_left_absorb: "(A & (A & B)) = (A & B)"
+  by blast
+
lemma eq_ac:
shows eq_commute: "(a=b) = (b=a)"
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
@@ -514,11 +526,15 @@
lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules

+subsubsection {* Actual Installation of the Simplifier *}
+
use "simpdata.ML"
setup Simplifier.setup
setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
setup Splitter.setup setup Clasimp.setup

+declare disj_absorb [simp] conj_absorb [simp]
+
lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
by blast+
```