History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Auth/ZhouGollmann.thy
Revision Date Author Comments
# ed7a971e 05-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# 5385dbfa 16-Jan-2018 wenzelm <none@none>

standardized towards new-style formal comments: isabelle update_comments;


# ce5e1da3 28-Dec-2015 wenzelm <none@none>

more symbols;


# feca4ab8 10-Dec-2015 wenzelm <none@none>

isabelle update_cartouches -c -t;


# 9fd71573 10-Jun-2014 Thomas Sewell <thomas.sewell@nicta.com.au>

Hypsubst preserves equality hypotheses

Fixes included for various theories affected by this change.

--HG--
extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0


# 713cd402 13-Mar-2014 nipkow <none@none>

enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions

--HG--
extra : rebase_source : 4103bf02b2df95e1e84808f766f131292beef893


# deac04eb 22-Jul-2010 wenzelm <none@none>

updated some headers;


# baea5702 01-Mar-2010 haftmann <none@none>

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)


# 079cde2d 17-Oct-2009 wenzelm <none@none>

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;


# 7b63d2a6 11-Jul-2007 berghofe <none@none>

Adapted to new inductive definition package.


# cd65d9bc 16-Nov-2006 wenzelm <none@none>

more robust syntax for definition/abbreviation/notation;


# 8d37dcbe 28-Sep-2006 wenzelm <none@none>

replaced syntax/translations by abbreviation;


# a7060872 17-Jun-2005 haftmann <none@none>

migrated theory headers to new format


# e6988de0 20-Jul-2004 paulson <none@none>

minor tweaks to go with the new version of the Accountability paper


# eb9e4051 15-Jul-2004 paulson <none@none>

redefining sumr to be a translation to setsum


# 5cd532fe 12-May-2004 paulson <none@none>

simpilified and strengthened proofs


# fd8083e7 11-May-2004 paulson <none@none>

broken no longer includes TTP, and other minor changes


# 5442a36e 26-Sep-2003 paulson <none@none>

Conversion of all main protocols from "Shared" to "Public".
Removal of Key_supply_ax: modifications to possibility theorems.
Improved presentation.


# 1b3f1e57 12-Aug-2003 paulson <none@none>

possibility proof!


# 05eb17d2 12-Aug-2003 paulson <none@none>

ZhouGollmann: new example (fair non-repudiation protocol)