equal
deleted
inserted
replaced
64 |
64 |
65 (**** Conversion ****) |
65 (**** Conversion ****) |
66 |
66 |
67 consts |
67 consts |
68 Sconv1 :: "i" |
68 Sconv1 :: "i" |
69 "<-1->" :: "[i,i]=>o" (infixl 50) |
|
70 Sconv :: "i" |
69 Sconv :: "i" |
71 "<--->" :: "[i,i]=>o" (infixl 50) |
|
72 |
70 |
73 translations |
71 abbreviation |
74 "a<-1->b" == "<a,b> \<in> Sconv1" |
72 Sconv1_rel (infixl "<-1->" 50) where |
75 "a<--->b" == "<a,b> \<in> Sconv" |
73 "a<-1->b == <a,b> \<in> Sconv1" |
|
74 |
|
75 abbreviation |
|
76 Sconv_rel (infixl "<--->" 50) where |
|
77 "a<--->b == <a,b> \<in> Sconv" |
76 |
78 |
77 inductive |
79 inductive |
78 domains "Sconv1" <= "lambda*lambda" |
80 domains "Sconv1" <= "lambda*lambda" |
79 intros |
81 intros |
80 red1: "m -1-> n ==> m<-1->n" |
82 red1: "m -1-> n ==> m<-1->n" |