equal
deleted
inserted
replaced
72 Sred :: "i" |
72 Sred :: "i" |
73 Spar_red1 :: "i" |
73 Spar_red1 :: "i" |
74 Spar_red :: "i" |
74 Spar_red :: "i" |
75 |
75 |
76 abbreviation |
76 abbreviation |
77 Sred1_rel (infixl "-1->" 50) where |
77 Sred1_rel (infixl \<open>-1->\<close> 50) where |
78 "a -1-> b == <a,b> \<in> Sred1" |
78 "a -1-> b == <a,b> \<in> Sred1" |
79 |
79 |
80 abbreviation |
80 abbreviation |
81 Sred_rel (infixl "-\<longrightarrow>" 50) where |
81 Sred_rel (infixl \<open>-\<longrightarrow>\<close> 50) where |
82 "a -\<longrightarrow> b == <a,b> \<in> Sred" |
82 "a -\<longrightarrow> b == <a,b> \<in> Sred" |
83 |
83 |
84 abbreviation |
84 abbreviation |
85 Spar_red1_rel (infixl "=1=>" 50) where |
85 Spar_red1_rel (infixl \<open>=1=>\<close> 50) where |
86 "a =1=> b == <a,b> \<in> Spar_red1" |
86 "a =1=> b == <a,b> \<in> Spar_red1" |
87 |
87 |
88 abbreviation |
88 abbreviation |
89 Spar_red_rel (infixl "===>" 50) where |
89 Spar_red_rel (infixl \<open>===>\<close> 50) where |
90 "a ===> b == <a,b> \<in> Spar_red" |
90 "a ===> b == <a,b> \<in> Spar_red" |
91 |
91 |
92 |
92 |
93 inductive |
93 inductive |
94 domains "Sred1" \<subseteq> "lambda*lambda" |
94 domains "Sred1" \<subseteq> "lambda*lambda" |