# HG changeset patch
# User wenzelm
# Date 1444488043 -7200
# Node ID 6762c84451385086855dd38354d804258b665176
# Parent  efac889fccbcfa34f01aa605a92635382fe1d87b
use Isabelle symbols by default;

diff -r efac889fccbc -r 6762c8445138 src/HOL/Library/Rewrite.thy
--- a/src/HOL/Library/Rewrite.thy	Sat Oct 10 16:26:23 2015 +0200
+++ b/src/HOL/Library/Rewrite.thy	Sat Oct 10 16:40:43 2015 +0200
@@ -8,9 +8,7 @@
 imports Main
 begin
 
-consts rewrite_HOLE :: "'a::{}"
-notation rewrite_HOLE ("HOLE")
-notation rewrite_HOLE ("\<hole>")
+consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
 
 lemma eta_expand:
   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
@@ -25,7 +23,8 @@
   done
 
 lemma imp_cong_eq:
-  "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv> ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
+  "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv>
+    ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
   apply (intro Pure.equal_intr_rule)
      apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+