Skip to content
Success

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. proper setup for rule attribute;
  3. more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
  4. clarified output of embedded values, e.g. for 'print_locale';
  5. tuned: more antiquotations;
  6. tuned;
  7. tuned signature: more position information;
  8. tuned;
Changeset 78101:300537844bb7 by wenzelm:
merged
Changeset 78100:35439ca0133c by wenzelm:
proper setup for rule attribute;
The file was modified src/HOL/Decision_Procs/Conversions.thy
Changeset 78099:4d9349989d94 by wenzelm:
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
The file was modified src/Doc/Isar_Ref/Generic.thy
The file was modified src/HOL/Bali/Eval.thy
The file was modified src/HOL/Bali/Evaln.thy
The file was modified src/HOL/Bali/WellType.thy
The file was modified src/HOL/Boolean_Algebras.thy
The file was modified src/HOL/Data_Structures/Less_False.thy
The file was modified src/HOL/Enum.thy
The file was modified src/HOL/Finite_Set.thy
The file was modified src/HOL/Fun.thy
The file was modified src/HOL/Groups.thy
The file was modified src/HOL/HOL.thy
The file was modified src/HOL/HOLCF/Cfun.thy
The file was modified src/HOL/HOLCF/Pcpo.thy
The file was modified src/HOL/Library/Extended_Nat.thy
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy
The file was modified src/HOL/Library/Multiset.thy
The file was modified src/HOL/Library/Multiset_Order.thy
The file was modified src/HOL/List.thy
The file was modified src/HOL/Nat.thy
The file was modified src/HOL/Nonstandard_Analysis/NSA.thy
The file was modified src/HOL/Num.thy
The file was modified src/HOL/Numeral_Simprocs.thy
The file was modified src/HOL/Product_Type.thy
The file was modified src/HOL/Set.thy
The file was modified src/ZF/OrdQuant.thy
The file was modified src/ZF/pair.thy
Changeset 78098:2cd7e5518d0d by wenzelm:
clarified output of embedded values, e.g. for 'print_locale';
The file was modified src/Pure/Isar/attrib.ML
The file was modified src/Pure/Isar/token.ML
Changeset 78097:2ea20bb1493c by wenzelm:
tuned: more antiquotations;
The file was modified src/HOL/Nominal/nominal_inductive.ML
Changeset 78096:838198d17a40 by wenzelm:
tuned;
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy
The file was modified src/HOL/Eisbach/Tests.thy
Changeset 78095:bc42c074e58f by wenzelm:
tuned signature: more position information;
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy
The file was modified src/HOL/Eisbach/Tests.thy
The file was modified src/HOL/Eisbach/method_closure.ML
The file was modified src/HOL/HOLCF/Tools/fixrec.ML
The file was modified src/HOL/Library/adhoc_overloading.ML
The file was modified src/HOL/Nominal/nominal_inductive.ML
The file was modified src/HOL/Nominal/nominal_inductive2.ML
The file was modified src/HOL/Real_Asymp/exp_log_expression.ML
The file was modified src/HOL/Statespace/state_space.ML
The file was modified src/HOL/Tools/BNF/bnf_def.ML
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.ML
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
The file was modified src/HOL/Tools/Function/function.ML
The file was modified src/HOL/Tools/Lifting/lifting_def.ML
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML
The file was modified src/HOL/Tools/Quotient/quotient_def.ML
The file was modified src/HOL/Tools/Quotient/quotient_type.ML
The file was modified src/HOL/Tools/Transfer/transfer_bnf.ML
The file was modified src/HOL/Tools/functor.ML
The file was modified src/HOL/Tools/inductive.ML
The file was modified src/HOL/Tools/inductive_set.ML
The file was modified src/HOL/Tools/semiring_normalizer.ML
The file was modified src/HOL/Tools/typedef.ML
The file was modified src/Provers/order_tac.ML
The file was modified src/Pure/Isar/attrib.ML
The file was modified src/Pure/Isar/bundle.ML
The file was modified src/Pure/Isar/code.ML
The file was modified src/Pure/Isar/entity.ML
The file was modified src/Pure/Isar/expression.ML
The file was modified src/Pure/Isar/generic_target.ML
The file was modified src/Pure/Isar/isar_cmd.ML
The file was modified src/Pure/Isar/local_theory.ML
The file was modified src/Pure/Isar/locale.ML
The file was modified src/Pure/Isar/method.ML
The file was modified src/Pure/Isar/spec_rules.ML
The file was modified src/Pure/ex/Def.thy
The file was modified src/Pure/simplifier.ML
Changeset 78094:c3efa0b63d2e by wenzelm:
tuned;
The file was modified src/Pure/Admin/isabelle_cronjob.scala

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. prefer @{attributes} antiquotation over Attrib.internal; adapted to Isabelle/bc42c074e58f;
  3. tuned proofs;
Changeset 13484:91c7c75dea9e by wenzelm:
merged
Changeset 13483:ae5dec7716f4 by wenzelm:
prefer @{attributes} antiquotation over Attrib.internal;<br>adapted to Isabelle/bc42c074e58f;
The file was modified thys/Applicative_Lifting/applicative.ML
The file was modified thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy
The file was modified thys/Collections/ICF/tools/Locale_Code.thy
The file was modified thys/ConcurrentIMP/cimp.ML
The file was modified thys/Conditional_Transfer_Rule/CTR/CTR_Postprocessing.ML
The file was modified thys/Conditional_Transfer_Rule/CTR/CTR_Relators.ML
The file was modified thys/Conditional_Transfer_Rule/CTR/Tests/CTR_Tests.thy
The file was modified thys/Constructor_Funs/constructor_funs.ML
The file was modified thys/Deriving/Comparator_Generator/comparator_generator.ML
The file was modified thys/Deriving/Equality_Generator/equality_generator.ML
The file was modified thys/Deriving/Hash_Generator/hash_generator.ML
The file was modified thys/Dict_Construction/class_graph.ML
The file was modified thys/Dict_Construction/dict_construction.ML
The file was modified thys/Dict_Construction/side_conditions.ML
The file was modified thys/First_Order_Terms/Term.thy
The file was modified thys/IMP2/lib/named_simpsets.ML
The file was modified thys/Lazy_Case/lazy_case.ML
The file was modified thys/Monad_Memo_DP/transform/Transform_Data.ML
The file was modified thys/Nominal2/Nominal2.thy
The file was modified thys/Nominal2/nominal_atoms.ML
The file was modified thys/Nominal2/nominal_eqvt.ML
The file was modified thys/Nominal2/nominal_function.ML
The file was modified thys/Nominal2/nominal_inductive.ML
The file was modified thys/Nominal2/nominal_termination.ML
The file was modified thys/Randomised_Social_Choice/Automation/Preference_Profile_Cmd.thy
The file was modified thys/Show/show_generator.ML
The file was modified thys/Simpl/hoare.ML
The file was modified thys/Types_To_Sets_Extension/ETTS/ETTS_Substitution.ML
The file was modified thys/X86_Semantics/X86_Parse.ML
Changeset 13482:a023f98be016 by wenzelm:
tuned proofs;
The file was modified thys/HOLCF-Prelude/Data_Integer.thy
The file was modified thys/HOLCF-Prelude/Data_List.thy
The file was modified thys/HOLCF-Prelude/Data_Maybe.thy
The file was modified thys/HOLCF-Prelude/Data_Tuple.thy
The file was modified thys/HOLCF-Prelude/Definedness.thy
The file was modified thys/HOLCF-Prelude/Type_Classes.thy
The file was modified thys/HOLCF-Prelude/examples/HLint.thy