| author | wenzelm |
| Sun, 08 Jun 2008 14:29:09 +0200 | |
| changeset 27090 | 2f45c1b1b05d |
| parent 25722 | 0a104ddb72d9 |
| child 27623 | 8e9c19529a4e |
| permissions | -rw-r--r-- |
(* Title: HOL/Nominal/Examples/ROOT.ML ID: $Id$ Author: Christian Urban, TU Muenchen Various examples involving nominal datatypes. *) use_thys [ "CR", "CR_Takahashi", "Class", "Compile", "Fsub", "Height", "Lambda_mu", "SN", "Weakening", "Crary", "SOS", "LocalWeakening", "Support", "Contexts" ]; setmp quick_and_dirty true use_thy "VC_Condition";