moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
theory loader: reduced warnings -- thy database can be bypassed in certain situations;
Proof/Local_Theory.propagate_ml_env;
ML use function: propagate ML environment as well;
pervasive type generic_theory;
(* Author: Christian Urban TU Muenchen *)
header {* Various examples involving nominal datatypes. *}
theory Nominal_Examples
imports
CK_Machine
CR
CR_Takahashi
Class3
Compile
Contexts
Crary
Fsub
Height
Lambda_mu
LocalWeakening
Pattern
SN
SOS
Standardization
Support
Type_Preservation
W
Weakening
begin
end