Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

Added metadata for previous commit (Optics).
Addition of theorems throughout, particularly for prisms. New "chantype" command allows the definition of an algebraic datatype with generated prisms. New "dataspace" command allows the definition of a local-based state space, including lenses and prisms. Addition of various examples.

Changeset 11591:5a13e3f6bce8 by simon foster _simon.foster@york.ac.uk_: Added metadata for previous commit (Optics).
The file was modified	`metadata/metadata`
Changeset 11590:fa453ac871a2 by simon foster _simon.foster@york.ac.uk_: Addition of theorems throughout, particularly for prisms.<br>New "chantype" command allows the definition of an algebraic datatype with generated prisms.<br>New "dataspace" command allows the definition of a local-based state space, including lenses and prisms.<br>Addition of various examples.
The file was added	`thys/Optics/Channel_Type.ML`
The file was added	`thys/Optics/Channel_Type.thy`
The file was added	`thys/Optics/Channel_Type_Example.thy`
The file was added	`thys/Optics/Dataspace.ML`
The file was added	`thys/Optics/Dataspace.thy`
The file was added	`thys/Optics/Dataspace_Example.thy`
The file was added	`thys/Optics/Dataspaces.thy`
The file was added	`thys/Optics/Lens_Lib.ML`
The file was added	`thys/Optics/Lens_Statespace.ML`
The file was added	`thys/Optics/Lens_Statespace_Example.thy`
The file was added	`thys/Optics/Prism_Lib.ML`
The file was added	`thys/Optics/Prisms_Examples.thy`
The file was modified	`thys/Optics/Lens_Algebra.thy`
The file was modified	`thys/Optics/Lens_Instances.thy`
The file was modified	`thys/Optics/Lens_Order.thy`
The file was modified	`thys/Optics/Lens_Record.ML`
The file was modified	`thys/Optics/Optics.thy`
The file was modified	`thys/Optics/Prisms.thy`
The file was modified	`thys/Optics/ROOT`
The file was modified	`thys/Optics/Scenes.thy`
The file was modified	`thys/Optics/Two.thy`