ARM/v7/armSyntax.sml

31   Term.inst [Type.alpha |->
93     Term.inst [Type.alpha |-> stringSyntax.string_ty] s)
98     [Type.alpha |-> Term.type_of v,
99      Type.beta |-> Term.type_of s] valuestate_tm, [v,s])
103   HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t)
108     [Type.alpha |-> dest_monad_type (Term.type_of f),
109      Type.beta  |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g]
115     [Type.alpha |-> dest_monad_type (Term.type_of f),
116      Type.beta  |-> dest_monad_type (Term.type_of g)] parT_tm,[f,g])
121     [Type.alpha |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) f]
127     [Type.alpha |-> snd (dom_rng (Term.type_of f))] readT_tm, f)
136     [Term.inst [Type.alpha |-> ``:iiid``] ii,
137      Term.inst [Type.alpha |-> ``:RName``] r])
142     [Term.inst [Type.alpha |-> ``:iiid``] ii,
143      Term.inst [Type.alpha |-> ``:RName``] r,
149     [Term.inst [Type.alpha |-> ``:iiid``] ii,
150      Term.inst [Type.alpha |-> ``:PSRName``] r])
155     [Term.inst [Type.alpha |-> ``:iiid``] ii,
156      Term.inst [Type.alpha |-> ``:PSRName``] r,
157      Term.inst [Type.alpha |-> ``:ARMpsr``] v])
162     [Term.inst [Type.alpha |-> ``:iiid``] ii,
168     [Term.inst [Type.alpha |-> ``:iiid``] ii,
175     [Term.inst [Type.alpha |-> ``:iiid``] ii,
182     [Term.inst [Type.alpha |-> ``:iiid``] ii,
189   HolKernel.mk_comb(read_cpsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
194     [Term.inst [Type.alpha |-> ``:iiid``] ii,
195      Term.inst [Type.alpha |-> ``:ARMpsr``] v])
199   HolKernel.mk_comb(read_spsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
204     [Term.inst [Type.alpha |-> ``:iiid``] ii,
205      Term.inst [Type.alpha |-> ``:ARMpsr``] v])
210     [Term.inst [Type.alpha |-> ``:iiid``] ii,
213         Term.inst [Type.alpha |-> ``:num``] s)])
218     [Term.inst [Type.alpha |-> ``:iiid``] ii,
221         Term.inst [Type.alpha |-> ``:num``] s),
227     Term.inst [Type.alpha |-> ``:iiid``] ii)
231   HolKernel.mk_comb(send_event_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
236     Term.inst [Type.alpha |-> ``:iiid``] ii)
241     Term.inst [Type.alpha |-> ``:iiid``] ii)
254     [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] align_tm,
260     [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] aligned_tm,
266   [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] ITAdvance_tm, w)