Changes

Summary

merged
adapted to devel

Changeset 9397:0454be45c0e9 by nipkow: merged
Changeset 9396:dfac4403877c by nipkow: adapted to devel
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Containers/Mapping_Impl.thy` (diff)
The file was modified	`thys/CoreC++/Conform.thy` (diff)
The file was modified	`thys/CoreC++/Exceptions.thy` (diff)
The file was modified	`thys/CoreC++/Execute.thy` (diff)
The file was modified	`thys/CoreC++/TypeSafe.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Type_Systems/Compositionality.thy` (diff)
The file was modified	`thys/Featherweight_OCL/UML_State.thy` (diff)
The file was modified	`thys/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_UML.thy` (diff)
The file was modified	`thys/Featherweight_OCL/examples/Employee_Model/Design/Design_UML.thy` (diff)
The file was modified	`thys/FinFun/FinFun.thy` (diff)
The file was modified	`thys/Jinja/Common/Conform.thy` (diff)
The file was modified	`thys/Jinja/Common/Exceptions.thy` (diff)
The file was modified	`thys/Jinja/Common/Objects.thy` (diff)
The file was modified	`thys/Jinja/Common/TypeRel.thy` (diff)
The file was modified	`thys/Jinja/J/TypeSafe.thy` (diff)
The file was modified	`thys/Jinja/J/execute_Bigstep.thy` (diff)
The file was modified	`thys/Jinja/J/execute_WellType.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl3.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/Missing_Lemmas.thy` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Equivalence.thy` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Proof.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m1_auth.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m2_auth_chan.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m2_confid_chan.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m3_enc.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m3_sig.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_kerberos.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist_iirn.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist_inrn.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_kerberos.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_ds_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos4.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos5.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_nssk_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Runs.thy` (diff)
The file was modified	`thys/Statecharts/Contrib.thy` (diff)
The file was modified	`thys/Statecharts/HA.thy` (diff)
The file was modified	`thys/Statecharts/HAOps.thy` (diff)
The file was modified	`thys/Statecharts/HASem.thy` (diff)
The file was modified	`thys/Statecharts/Kripke.thy` (diff)
The file was modified	`thys/UPF/ElementaryPolicies.thy` (diff)
The file was modified	`thys/UPF/Service.thy` (diff)
The file was modified	`thys/UPF/ServiceExample.thy` (diff)
The file was modified	`thys/UPF/UPFCore.thy` (diff)