equal
deleted
inserted
replaced
1082 "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.minus_nat" |
1082 "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.minus_nat" |
1083 "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.times_nat" |
1083 "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.times_nat" |
1084 "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_nat" |
1084 "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_nat" |
1085 "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_eq_nat" |
1085 "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_eq_nat" |
1086 "OperationalEquality.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.eq_nat" |
1086 "OperationalEquality.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.eq_nat" |
|
1087 nat_rec "IntDef.nat_rec" |
|
1088 nat_case "IntDef.nat_case" |
1087 |
1089 |
1088 end |
1090 end |