equal
deleted
inserted
replaced
502 (*.from a list of fun-definitions "f x = ..." as 2nd argument |
502 (*.from a list of fun-definitions "f x = ..." as 2nd argument |
503 filter the elements with the same fun-identfier in "f y" |
503 filter the elements with the same fun-identfier in "f y" |
504 as the fst argument; |
504 as the fst argument; |
505 this is, because Isabelles filter takes more than 1 sec.*) |
505 this is, because Isabelles filter takes more than 1 sec.*) |
506 fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2 |
506 fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2 |
507 | same_funid f1 t = raise error ("same_funid called with t = (" |
507 | same_funid f1 t = error ("same_funid called with t = (" |
508 ^term2str f1^") ("^term2str t^")"); |
508 ^term2str f1^") ("^term2str t^")"); |
509 (*("filter_sameFunId" ,("Atools.filter'_sameFunId", |
509 (*("filter_sameFunId" ,("Atools.filter'_sameFunId", |
510 eval_filter_sameFunId "Atools.filter'_sameFunId"))*) |
510 eval_filter_sameFunId "Atools.filter'_sameFunId"))*) |
511 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId" |
511 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId" |
512 (p as Const ("Atools.filter'_sameFunId",_) $ |
512 (p as Const ("Atools.filter'_sameFunId",_) $ |