Skip to content
Success

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. add applicative instance for filters
Changeset 9612:73acb221a89c by Andreas Lochbihler:
merged
Changeset 9611:7a0d8c1f29ed by Andreas Lochbihler:
add applicative instance for filters
The file was addedthys/Applicative_Lifting/Applicative_Filter.thy
The file was modified thys/Applicative_Lifting/Applicative_Functor.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. add lemmas about prod_filter
Changeset 68667:96aae7c44bb2 by Andreas Lochbihler:
add lemmas about prod_filter
The file was modified src/HOL/Filter.thy