src/HOL/Old_Number_Theory/BijectionRel.thy
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/BijectionRel.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/BijectionRel.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -3,18 +3,18 @@
     1.4      Copyright   2000  University of Cambridge
     1.5  *)
     1.6  
     1.7 -section {* Bijections between sets *}
     1.8 +section \<open>Bijections between sets\<close>
     1.9  
    1.10  theory BijectionRel
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16    Inductive definitions of bijections between two different sets and
    1.17    between the same set.  Theorem for relating the two definitions.
    1.18  
    1.19    \bigskip
    1.20 -*}
    1.21 +\<close>
    1.22  
    1.23  inductive_set
    1.24    bijR :: "('a => 'b => bool) => ('a set * 'b set) set"
    1.25 @@ -24,10 +24,10 @@
    1.26  | insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
    1.27      ==> (insert a A, insert b B) \<in> bijR P"
    1.28  
    1.29 -text {*
    1.30 +text \<open>
    1.31    Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"}
    1.32    (and similar for @{term A}).
    1.33 -*}
    1.34 +\<close>
    1.35  
    1.36  definition
    1.37    bijP :: "('a => 'a => bool) => 'a set => bool" where
    1.38 @@ -51,7 +51,7 @@
    1.39      ==> insert a (insert b A) \<in> bijER P"
    1.40  
    1.41  
    1.42 -text {* \medskip @{term bijR} *}
    1.43 +text \<open>\medskip @{term bijR}\<close>
    1.44  
    1.45  lemma fin_bijRl: "(A, B) \<in> bijR P ==> finite A"
    1.46    apply (erule bijR.induct)
    1.47 @@ -100,7 +100,7 @@
    1.48    done
    1.49  
    1.50  
    1.51 -text {* \medskip @{term bijER} *}
    1.52 +text \<open>\medskip @{term bijER}\<close>
    1.53  
    1.54  lemma fin_bijER: "A \<in> bijER P ==> finite A"
    1.55    apply (erule bijER.induct)