| author | blanchet |
| Wed, 17 Sep 2014 11:12:46 +0200 | |
| changeset 58356 | 2f04f1fd28aa |
| parent 58329 | a31404ec7414 |
| child 58889 | 5b7a9633cfa8 |
| permissions | -rw-r--r-- |
(* Author: Christian Urban TU Muenchen *) header {* Various examples involving nominal datatypes. *} theory Nominal_Examples_Base imports CK_Machine CR CR_Takahashi Compile Contexts Crary Fsub Height Lambda_mu LocalWeakening Pattern SN SOS Standardization Support Type_Preservation W Weakening begin end