refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
(* 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