src/HOL/Nominal/Examples/Nominal_Examples.thy
author blanchet
Fri, 16 Apr 2010 16:54:05 +0200
changeset 36186 bd246b00ef5a
parent 33189 82a40677c1f8
child 36277 9be4ab2acc13
permissions -rw-r--r--
restore order of clauses in TPTP output; there's a rather subtle invariant w.r.t. "extract_lemmas"

(*  Author:  Christian Urban TU Muenchen *)

header {* Various examples involving nominal datatypes. *}

theory Nominal_Examples
imports
  CR
  CR_Takahashi
  Class
  Compile
  Fsub
  Height
  Lambda_mu
  SN
  Weakening
  Crary
  SOS
  LocalWeakening
  Support
  Contexts
  Standardization
  W
  Pattern
begin

end