Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/PER.thy
changeset 61933 cf58b5b794b2
parent 61260 e6f03fae14d5
child 69597 ff784d5a5bfb 
--- a/src/HOL/ex/PER.thy	Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/PER.thy	Sat Dec 26 15:59:27 2015 +0100
@@ -11,8 +11,8 @@
 text \<open>
   Higher-order quotients are defined over partial equivalence
   relations (PERs) instead of total ones.  We provide axiomatic type
-  classes @{text "equiv < partial_equiv"} and a type constructor
-  @{text "'a quot"} with basic operations.  This development is based
+  classes \<open>equiv < partial_equiv\<close> and a type constructor
+  \<open>'a quot\<close> with basic operations.  This development is based
   on:
 
   Oscar Slotosch: \emph{Higher Order Quotients and their
@@ -25,9 +25,9 @@
 subsection \<open>Partial equivalence\<close>
 
 text \<open>
-  Type class @{text partial_equiv} models partial equivalence
-  relations (PERs) using the polymorphic @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow>
-  bool"} relation, which is required to be symmetric and transitive,
+  Type class \<open>partial_equiv\<close> models partial equivalence
+  relations (PERs) using the polymorphic \<open>\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow>
+  bool\<close> relation, which is required to be symmetric and transitive,
   but not necessarily reflexive.
 \<close>
 
@@ -64,7 +64,7 @@
 subsection \<open>Equivalence on function spaces\<close>
 
 text \<open>
-  The @{text \<sim>} relation is lifted to function spaces.  It is
+  The \<open>\<sim>\<close> relation is lifted to function spaces.  It is
   important to note that this is \emph{not} the direct product, but a
   structural one corresponding to the congruence property.
 \<close>
@@ -117,8 +117,8 @@
 
 text \<open>
   The class of total equivalence relations on top of PERs.  It
-  coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
-  :: 'a \<Rightarrow> 'a \<Rightarrow> bool"} is required to be reflexive, transitive and
+  coincides with the standard notion of equivalence, i.e.\ \<open>\<sim>
+  :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close> is required to be reflexive, transitive and
   symmetric.
 \<close>
 
@@ -148,7 +148,7 @@
 subsection \<open>Quotient types\<close>
 
 text \<open>
-  The quotient type @{text "'a quot"} consists of all
+  The quotient type \<open>'a quot\<close> consists of all
   \emph{equivalence classes} over elements of the base type @{typ 'a}.
 \<close>
isabelle