Skip to content
Success

Changes

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 (diff)
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 (diff)
The file was modified src/HOL/Bali/Eval.thy (diff)
The file was modified src/HOL/Bali/Evaln.thy (diff)
The file was modified src/HOL/Bali/WellType.thy (diff)
The file was modified src/HOL/Boolean_Algebras.thy (diff)
The file was modified src/HOL/Data_Structures/Less_False.thy (diff)
The file was modified src/HOL/Enum.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/HOLCF/Cfun.thy (diff)
The file was modified src/HOL/HOLCF/Pcpo.thy (diff)
The file was modified src/HOL/Library/Extended_Nat.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSA.thy (diff)
The file was modified src/HOL/Num.thy (diff)
The file was modified src/HOL/Numeral_Simprocs.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/ZF/OrdQuant.thy (diff)
The file was modified src/ZF/pair.thy (diff)
Changeset 78098:2cd7e5518d0d by wenzelm:
clarified output of embedded values, e.g. for 'print_locale';
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
Changeset 78097:2ea20bb1493c by wenzelm:
tuned: more antiquotations;
The file was modified src/HOL/Nominal/nominal_inductive.ML (diff)
Changeset 78096:838198d17a40 by wenzelm:
tuned;
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/HOL/Eisbach/Tests.thy (diff)
Changeset 78095:bc42c074e58f by wenzelm:
tuned signature: more position information;
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/HOL/Eisbach/Tests.thy (diff)
The file was modified src/HOL/Eisbach/method_closure.ML (diff)
The file was modified src/HOL/HOLCF/Tools/fixrec.ML (diff)
The file was modified src/HOL/Library/adhoc_overloading.ML (diff)
The file was modified src/HOL/Nominal/nominal_inductive.ML (diff)
The file was modified src/HOL/Nominal/nominal_inductive2.ML (diff)
The file was modified src/HOL/Real_Asymp/exp_log_expression.ML (diff)
The file was modified src/HOL/Statespace/state_space.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_def.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Quotient/quotient_def.ML (diff)
The file was modified src/HOL/Tools/Quotient/quotient_type.ML (diff)
The file was modified src/HOL/Tools/Transfer/transfer_bnf.ML (diff)
The file was modified src/HOL/Tools/functor.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/inductive_set.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
The file was modified src/HOL/Tools/typedef.ML (diff)
The file was modified src/Provers/order_tac.ML (diff)
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/bundle.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/Isar/entity.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/Isar/isar_cmd.ML (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/Isar/spec_rules.ML (diff)
The file was modified src/Pure/ex/Def.thy (diff)
The file was modified src/Pure/simplifier.ML (diff)
Changeset 78094:c3efa0b63d2e by wenzelm:
tuned;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)