Lines Matching defs:Term
1 structure Term :> Term =
10 val ERR = mk_HOL_ERR "Term"
11 val WARN = HOL_WARNING "Term"
202 | dest_var _ = raise ERR "dest_var" "Term not a variable"
205 | dest_const _ = raise ERR "dest_const" "Term not a constant"
212 | _ => raise ERR "dest_thy_const" "Term not a constant"
216 | dest_comb _ = raise ERR "dest_comb" "Term not a comb"
222 | dest_abs _ = raise ERR "dest_abs" "Term not an abstraction"
417 | _ => raise ERR "var_occurs" "Term not a variable"
810 raise ERR "beta_conv" "Term not an application"
817 else raise ERR "eta_conv" "Term not an eta-redex"
819 raise ERR "eta_conv" "Term not an eta-redex"
864 | _ => raise ERR "rename_bvar" "Term not an abstraction"
1039 else raise ERR "dest_eq_ty" "Term not an equality"