Changes

Summary

eliminated spurious diagnostic commands -- make this work with skip_proofs;

Changeset 8544:7a8a63f46f76 by wenzelm: eliminated spurious diagnostic commands -- make this work with skip_proofs;
The file was modified	`thys/Amortized_Complexity/Splay_Tree_Analysis_Optimal.thy` (diff)
The file was modified	`thys/Buchi_Complementation/Complementation.thy` (diff)
The file was modified	`thys/CRDT/RGA.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/MapGA.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Type_Systems/TypeSystem.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Det.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_IArrays.thy` (diff)
The file was modified	`thys/FLP/Execution.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_Skeleton.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Transform.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics.thy` (diff)
The file was modified	`thys/Launchbury/CorrectnessOriginal.thy` (diff)
The file was modified	`thys/Launchbury/CorrectnessResourced.thy` (diff)
The file was modified	`thys/List_Update/BIT.thy` (diff)
The file was modified	`thys/List_Update/Move_to_Front.thy` (diff)
The file was modified	`thys/List_Update/OPT2.thy` (diff)
The file was modified	`thys/List_Update/RExp_Var.thy` (diff)
The file was modified	`thys/LocalLexing/LocalLexingLemmas.thy` (diff)
The file was modified	`thys/LocalLexing/TheoremD14.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subgraph.thy` (diff)
The file was modified	`thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy` (diff)
The file was modified	`thys/Prpu_Maxflow/Prpu_Common_Impl.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Foreach.thy` (diff)
The file was modified	`thys/pGCL/Misc.thy` (diff)