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/Decision_Procs/Commutative_Ring.thy
changeset 80914 d97fdabd9e2b
parent 78795 f7e972d567f3 
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -106,7 +106,7 @@
 
 text \<open>Defining the basic ring operations on normalized polynomials\<close>
 
-function add :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>+\<rangle>" 65)
+function add :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl \<open>\<langle>+\<rangle>\<close> 65)
   where
     "Pc a \<langle>+\<rangle> Pc b = Pc (a + b)"
   | "Pc c \<langle>+\<rangle> Pinj i P = Pinj i (P \<langle>+\<rangle> Pc c)"
@@ -132,7 +132,7 @@
   by pat_completeness auto
 termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
 
-function mul :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>*\<rangle>" 70)
+function mul :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl \<open>\<langle>*\<rangle>\<close> 70)
   where
     "Pc a \<langle>*\<rangle> Pc b = Pc (a * b)"
   | "Pc c \<langle>*\<rangle> Pinj i P =
@@ -174,7 +174,7 @@
   | "neg (PX P x Q) = PX (neg P) x (neg Q)"
 
 text \<open>Subtraction\<close>
-definition sub :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>-\<rangle>" 65)
+definition sub :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl \<open>\<langle>-\<rangle>\<close> 65)
   where "sub P Q = P \<langle>+\<rangle> neg Q"
 
 text \<open>Square for Fast Exponentiation\<close>
isabelle