Changes

Summary

tuned proofs, to allow unfold_abs_def;
tuned;

Changeset 6745:8f666ad1379d by wenzelm: tuned proofs, to allow unfold_abs_def;
The file was modified	`thys/Abstract-Rewriting/Abstract_Rewriting.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Polygon.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Bivariate_Polynomials.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)
The file was modified	`thys/Coinductive_Languages/Coinductive_Language.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/SetIndex.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams/Decreasing_Diagrams.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Det_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/Rings2.thy` (diff)
The file was modified	`thys/Formal_SSA/Construct_SSA_code.thy` (diff)
The file was modified	`thys/Formal_SSA/Construct_SSA_notriv_code.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Determinants2.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan_IArrays.thy` (diff)
The file was modified	`thys/Jinja/DFA/Err.thy` (diff)
The file was modified	`thys/Jinja/DFA/Kildall.thy` (diff)
The file was modified	`thys/Jinja/DFA/Semilat.thy` (diff)
The file was modified	`thys/Jinja/DFA/SemilatAlg.thy` (diff)
The file was modified	`thys/Jinja/DFA/Typing_Framework_err.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1JVMBisim.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Err.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Kildall.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Semilat.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/SemilatAlg.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Typing_Framework_err.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Compiler.thy` (diff)
The file was modified	`thys/KBPs/SPRViewNonDet.thy` (diff)
The file was modified	`thys/KBPs/SPRViewNonDetIndInit.thy` (diff)
The file was modified	`thys/LTL_to_DRA/DTS.thy` (diff)
The file was modified	`thys/LTL_to_DRA/LTL_FGXU.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Logical_Characterization.thy` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_to_GBA_impl.thy` (diff)
The file was modified	`thys/Launchbury/HOLCF-Join-Classes.thy` (diff)
The file was modified	`thys/List_Update/BIT.thy` (diff)
The file was modified	`thys/List_Update/MTF2_Effects.thy` (diff)
The file was modified	`thys/List_Update/OPT2.thy` (diff)
The file was modified	`thys/List_Update/TS.thy` (diff)
The file was modified	`thys/Lower_Semicontinuous/Lower_Semicontinuous.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/M2L.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Derivatives.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Regular_Exp.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Regular_Operators.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/WS1S.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/One_Step_Method.thy` (diff)
The file was modified	`thys/Planarity_Certificates/l4v/lib/wp/NonDetMonad.thy` (diff)
The file was modified	`thys/QR_Decomposition/IArray_Addenda_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/Least_Squares_Approximation.thy` (diff)
The file was modified	`thys/QR_Decomposition/Projections.thy` (diff)
The file was modified	`thys/ROBDD/Conc_Impl.thy` (diff)
The file was modified	`thys/ROBDD/Pointer_Map_Impl.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Mod_Type.thy` (diff)
The file was modified	`thys/Real_Impl/Real_Unique_Impl.thy` (diff)
The file was modified	`thys/Refine_Monadic/Generic/RefineG_Domain.thy` (diff)
The file was modified	`thys/Regex_Equivalence/Derivatives_Finite.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map.thy` (diff)
The file was modified	`thys/Sort_Encodings/G.thy` (diff)
The file was modified	`thys/Sort_Encodings/Mcalc.thy` (diff)
The file was modified	`thys/Sort_Encodings/Mcalc2C.thy` (diff)
The file was modified	`thys/Sort_Encodings/T.thy` (diff)
The file was modified	`thys/Sturm_Tarski/Sturm_Tarski.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Down.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Grid.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Up_Down.thy` (diff)
The file was modified	`thys/Verified-Prover/Prover.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/Universes.thy` (diff)
The file was modified	`thys/pGCL/Healthiness.thy` (diff)
The file was modified	`thys/pGCL/LoopInduction.thy` (diff)
The file was modified	`thys/pGCL/Loops.thy` (diff)
Changeset 6744:a4d69e985ed9 by wenzelm: tuned;
The file was modified	`thys/Decreasing-Diagrams/ROOT` (diff)
The file was modified	`thys/Perron_Frobenius/ROOT` (diff)