| changeset 48041 | d60f6b41bf2d |
| parent 48038 | 72a8506dd59b |
| child 48059 | f6ce99d3719b |
--- a/src/HOL/ex/FinFunPred.thy Wed May 30 10:04:05 2012 +0200 +++ b/src/HOL/ex/FinFunPred.thy Wed May 30 16:05:06 2012 +0200 @@ -4,7 +4,7 @@ Predicates modelled as FinFuns *} -theory FinFunPred imports "~~/src/HOL/Library/FinFun" begin +theory FinFunPred imports "~~/src/HOL/Library/FinFun_Syntax" begin text {* Instantiate FinFun predicates just like predicates *}