Thu, 24 Jul 2014 13:01:49 +0200 | kuncar | prevent beta-contraction in proving extra assumptions for abs_eq | changeset | files |
Thu, 24 Jul 2014 11:54:15 +0200 | wenzelm | more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy); | changeset | files |