equal
deleted
inserted
replaced
135 |
135 |
136 abbreviation |
136 abbreviation |
137 nil :: msg where |
137 nil :: msg where |
138 "nil == Number 0" |
138 "nil == Number 0" |
139 |
139 |
140 consts agl :: "msg set" |
140 inductive_set agl :: "msg set" |
141 |
141 where |
142 inductive agl |
142 Nil[intro]: "nil:agl" |
143 intros |
143 | Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl" |
144 Nil[intro]: "nil:agl" |
|
145 Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl" |
|
146 |
144 |
147 subsubsection{*basic facts about agent lists*} |
145 subsubsection{*basic facts about agent lists*} |
148 |
146 |
149 lemma del_in_agl [intro]: "I:agl ==> del (a,I):agl" |
147 lemma del_in_agl [intro]: "I:agl ==> del (a,I):agl" |
150 by (erule agl.induct, auto) |
148 by (erule agl.induct, auto) |