src/HOL/Auth/ROOT.ML

- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set and to_pred attributes, because it is no longer applied automatically
- Manually applied predicate1I in proof of accp_subset, because it is no longer
part of the claset
- Replaced psubset_def by less_le

(*  Title:      HOL/Auth/ROOT.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Root file for protocol proofs.
*)

no_document use_thy "NatPair";

use_thys [

(* Conventional protocols: rely on 
   conventional Message, Event and Public *)

(*Shared-key protocols*)
  "NS_Shared",
  "Kerberos_BAN",
  "Kerberos_BAN_Gets",
  "KerberosIV",
  "KerberosIV_Gets",
  "KerberosV",
  "OtwayRees",
  "OtwayRees_AN",
  "OtwayRees_Bad",
  "OtwayReesBella",
  "WooLam",
  "Recur",
  "Yahalom",
  "Yahalom2",
  "Yahalom_Bad",
  "ZhouGollmann",

(*Public-key protocols*)
  "NS_Public_Bad",
  "NS_Public",
  "TLS",
  "CertifiedEmail",

(*Smartcard protocols: rely on conventional Message and on new
  EventSC and Smartcard *)

  "Smartcard/ShoupRubin",
  "Smartcard/ShoupRubinBella",

(*Blanqui's "guard" concept: protocol-independent secrecy*)
  "Guard/P1",
  "Guard/P2",
  "Guard/Guard_NS_Public",
  "Guard/Guard_OtwayRees",
  "Guard/Guard_Yahalom",
  "Guard/Proto"
];