Skip to content
Success

Changes

Summary

  1. merged from afp-2016-1
  2. add `six` to sitegen requirements
  3. quiet installation with pip
  4. Optics: factor out example so proof document remains undisturbed
  5. add Optics to ROOTS
  6. Optics: uncomment example use of alphabet command so that it is tested
  7. new entry Optics
  8. New entry Security_Protocol_Refinement
Changeset 7971:b34fef7605f4 by lars hupel _lars.hupel@mytum.de_:
merged from afp-2016-1
Changeset 7970:0333f32fdf76 by lars hupel _lars.hupel@mytum.de_:
add `six` to sitegen requirements
The file was modified admin/sitegen-req.txt (diff)
Changeset 7969:d2d8010ad057 by lars hupel _lars.hupel@mytum.de_:
quiet installation with pip
The file was modified admin/sitegen (diff)
Changeset 7968:0765640be448 by gerwin.klein@data61.csiro.au:
Optics: factor out example so proof document remains undisturbed
The file was addedthys/Optics/Lens_Record_Example.thy
The file was modified thys/Optics/Lens_Instances.thy (diff)
The file was modified thys/Optics/ROOT (diff)
Changeset 7967:d7bc5e73ffac by gerwin.klein@data61.csiro.au:
add Optics to ROOTS
The file was modified thys/ROOTS (diff)
Changeset 7966:6ff9f26bc099 by gerwin.klein@data61.csiro.au:
Optics: uncomment example use of alphabet command so that it is tested
The file was modified thys/Optics/Lens_Instances.thy (diff)
Changeset 7965:f489cef4d525 by gerwin.klein@data61.csiro.au:
new entry Optics
The file was addedthys/Optics/Interp.thy
The file was addedthys/Optics/Lens_Algebra.thy
The file was addedthys/Optics/Lens_Instances.thy
The file was addedthys/Optics/Lens_Laws.thy
The file was addedthys/Optics/Lens_Order.thy
The file was addedthys/Optics/Lens_Record.ML
The file was addedthys/Optics/Lenses.thy
The file was addedthys/Optics/Prisms.thy
The file was addedthys/Optics/ROOT
The file was addedthys/Optics/Two.thy
The file was addedthys/Optics/document/comment.sty
The file was addedthys/Optics/document/document.sty
The file was addedthys/Optics/document/figures/Composition.pdf
The file was addedthys/Optics/document/figures/Independence.pdf
The file was addedthys/Optics/document/figures/Lens.pdf
The file was addedthys/Optics/document/figures/Sum.pdf
The file was addedthys/Optics/document/figures/parallel-by-merge.pdf
The file was addedthys/Optics/document/isabelle.sty
The file was addedthys/Optics/document/isabellesym.sty
The file was addedthys/Optics/document/isabelletags.sty
The file was addedthys/Optics/document/pdfsetup.sty
The file was addedthys/Optics/document/railsetup.sty
The file was addedthys/Optics/document/root.bib
The file was addedthys/Optics/document/root.tex
The file was addedweb/entries/Optics.shtml
The file was modified metadata/metadata (diff)
The file was modified web/index.shtml (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7964:ecf1fb1a623d by nipkow:
New entry Security_Protocol_Refinement
The file was addedthys/Security_Protocol_Refinement/Auth_simple/m1_auth.thy
The file was addedthys/Security_Protocol_Refinement/Auth_simple/m2_auth_chan.thy
The file was addedthys/Security_Protocol_Refinement/Auth_simple/m2_confid_chan.thy
The file was addedthys/Security_Protocol_Refinement/Auth_simple/m3_enc.thy
The file was addedthys/Security_Protocol_Refinement/Auth_simple/m3_sig.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m1_ds.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m1_kerberos.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m1_keydist.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m1_keydist_iirn.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m1_keydist_inrn.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m1_nssk.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m2_ds.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m2_kerberos.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m2_nssk.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m3_ds.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m3_ds_par.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m3_kerberos4.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m3_kerberos5.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m3_kerberos_par.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m3_nssk.thy
The file was addedthys/Security_Protocol_Refinement/Key_establish/m3_nssk_par.thy
The file was addedthys/Security_Protocol_Refinement/ROOT
The file was addedthys/Security_Protocol_Refinement/Refinement/Agents.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/Atoms.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/Channels.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/Infra.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/Keys.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/Message.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/Refinement.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/Runs.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/a0i_agree.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/a0n_agree.thy
The file was addedthys/Security_Protocol_Refinement/Refinement/s0g_secrecy.thy
The file was addedthys/Security_Protocol_Refinement/document/isapreamble.tex
The file was addedthys/Security_Protocol_Refinement/document/root.tex
The file was addedthys/Security_Protocol_Refinement/document/session_graph.tex
The file was addedweb/entries/Security_Protocol_Refinement.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)