equal
deleted
inserted
replaced
48 |
48 |
49 definition |
49 definition |
50 map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50) where |
50 map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50) where |
51 "(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)" |
51 "(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)" |
52 |
52 |
53 nonterminals |
53 nonterminal maplets and maplet |
54 maplets maplet |
|
55 |
54 |
56 syntax |
55 syntax |
57 "_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _") |
56 "_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _") |
58 "_maplets" :: "['a, 'a] => maplet" ("_ /[|->]/ _") |
57 "_maplets" :: "['a, 'a] => maplet" ("_ /[|->]/ _") |
59 "" :: "maplet => maplets" ("_") |
58 "" :: "maplet => maplets" ("_") |