changeset 35092 | cfe605c54e50 |
parent 34974 | 18b41bba42b5 |
child 37135 | 636e6d8645d6 |
--- a/src/HOL/Hoare/hoare_tac.ML Wed Feb 10 14:12:02 2010 +0100 +++ b/src/HOL/Hoare/hoare_tac.ML Wed Feb 10 14:12:04 2010 +0100 @@ -58,7 +58,7 @@ let val T as Type ("fun",[t,_]) = fastype_of trm in Collect_const t $ trm end; -fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT); +fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT); fun Mset ctxt prop =