# HG changeset patch
# User haftmann
# Date 1330815877 -3600
# Node ID 13a3657d0dacac2b80cca56da336a5ebb30ed1a4
# Parent  b778cc5396013b261e7d1a87ff53683401e3cba2
dropped dead code

diff -r b778cc539601 -r 13a3657d0dac src/HOL/Import/MakeEqual.thy
--- a/src/HOL/Import/MakeEqual.thy	Sun Mar 04 00:03:21 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*  Title:      HOL/Import/MakeEqual.thy
-    Author:     Sebastian Skalberg, TU Muenchen
-*)
-
-theory MakeEqual imports Main
-  uses "shuffler.ML" begin
-
-setup Shuffler.setup
-
-lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)"
-proof
-  assume "A & B ==> PROP C" A B
-  thus "PROP C"
-    by auto
-next
-  assume "[| A; B |] ==> PROP C" "A & B"
-  thus "PROP C"
-    by auto
-qed
-
-lemma imp_norm [shuffle_rule]: "(Trueprop (A --> B)) == (A ==> B)"
-proof
-  assume "A --> B" A
-  thus B ..
-next
-  assume "A ==> B"
-  thus "A --> B"
-    by auto
-qed
-
-lemma all_norm [shuffle_rule]: "(Trueprop (ALL x. P x)) == (!!x. P x)"
-proof
-  fix x
-  assume "ALL x. P x"
-  thus "P x" ..
-next
-  assume "!!x. P x"
-  thus "ALL x. P x"
-    ..
-qed
-
-lemma ex_norm [shuffle_rule]: "(EX x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)"
-proof
-  fix x
-  assume ex: "EX x. P x ==> PROP Q"
-  assume "P x"
-  hence "EX x. P x" ..
-  with ex show "PROP Q" .
-next
-  assume allx: "!!x. P x ==> PROP Q"
-  assume "EX x. P x"
-  hence p: "P (SOME x. P x)"
-    ..
-  from allx
-  have "P (SOME x. P x) ==> PROP Q"
-    .
-  with p
-  show "PROP Q"
-    by auto
-qed
-
-lemma eq_norm [shuffle_rule]: "Trueprop (t = u) == (t == u)"
-proof
-  assume "t = u"
-  thus "t == u" by simp
-next
-  assume "t == u"
-  thus "t = u"
-    by simp
-qed
-
-end