use Isabelle symbols by default;
authorwenzelm
Sat Oct 10 16:40:43 2015 +0200 (2015-10-10)
changeset 613836762c8445138
parent 61382 efac889fccbc
child 61384 9f5145281888
use Isabelle symbols by default;
src/HOL/Library/Rewrite.thy
     1.1 --- a/src/HOL/Library/Rewrite.thy	Sat Oct 10 16:26:23 2015 +0200
     1.2 +++ b/src/HOL/Library/Rewrite.thy	Sat Oct 10 16:40:43 2015 +0200
     1.3 @@ -8,9 +8,7 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -consts rewrite_HOLE :: "'a::{}"
     1.8 -notation rewrite_HOLE ("HOLE")
     1.9 -notation rewrite_HOLE ("\<hole>")
    1.10 +consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
    1.11  
    1.12  lemma eta_expand:
    1.13    fixes f :: "'a::{} \<Rightarrow> 'b::{}"
    1.14 @@ -25,7 +23,8 @@
    1.15    done
    1.16  
    1.17  lemma imp_cong_eq:
    1.18 -  "(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'))"
    1.19 +  "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv>
    1.20 +    ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
    1.21    apply (intro Pure.equal_intr_rule)
    1.22       apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    1.23     apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+