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)
```