Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. bit accessor and fundamental properties
  2. merged
  3. more informative spec rules: optional name; clarified signature; more thorough treatment of Thm.trim_context vs. Thm.transfer;
  4. proper theory context, e.g. for Thm.transfer;
  5. more structural integrity;
  6. tuned
  7. reduced imports; deleted unusewd minor lemmas for that purpose
  8. tuned
  9. reduced imports and removed unused material
  10. tuned
Changeset 71181:8331063570d6 by haftmann:
bit accessor and fundamental properties
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/ex/Bit_Operations.thy (diff)
The file was modified src/HOL/ex/Word.thy (diff)
Changeset 71180:65192ac7eaf2 by wenzelm:
merged
Changeset 71179:592e2afdd50c by wenzelm:
more informative spec rules: optional name;<br>clarified signature;<br>more thorough treatment of Thm.trim_context vs. Thm.transfer;
The file was modified src/HOL/Library/old_recdef.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_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_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/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_hol.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_collect.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_primrec.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.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/record.ML (diff)
The file was modified src/Pure/Isar/spec_rules.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
Changeset 71178:c7d4f2ab40b9 by wenzelm:
proper theory context, e.g. for Thm.transfer;
The file was modified src/Pure/Isar/generic_target.ML (diff)
Changeset 71177:71467e35fc3c by wenzelm:
more structural integrity;
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
The file was modified src/Pure/assumption.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 71176:6c208c2dca53 by nipkow:
tuned
The file was modified src/HOL/Analysis/Starlike.thy (diff)
Changeset 71175:a1e94be66bd6 by nipkow:
reduced imports; deleted unusewd minor lemmas for that purpose
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
Changeset 71174:7fac205dd737 by nipkow:
tuned
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modified src/HOL/Analysis/Convex.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lipschitz.thy (diff)
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
The file was modified src/HOL/Analysis/Riemann_Mapping.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Library/Cardinality.thy (diff)
Changeset 71173:caede3159e23 by nipkow:
reduced imports and removed unused material
The file was modified src/HOL/Analysis/Retracts.thy (diff)
Changeset 71172:575b3a818de5 by nipkow:
tuned
The file was modified src/HOL/Analysis/Abstract_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Limits.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Continuous_Function.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Continuous_Extension.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Locally.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Retracts.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)