Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
  3. Backed out changeset 1bc422c08209 -- obsolete in AFP/5d11846ac6ab;
  4. really keep lambdas in translation if only predicates are missing
  5. tune ATP settings
  6. Added triangular numbers
  7. keep Local_Theory.reset for now -- still required in many AFP sessions (amending 1c201e4792cb);
  8. merged
  9. use polyml-test-0a6ebca445fc by default: already quite stable;
  10. renamings and new material
  11. merged
  12. some renamings and a bit of new material
  13. slightly more conventional naming schema
  14. Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
Changeset 69721:ce36bed06dee by angeliki koutsoukouargyraki _ak2110@cam.ac.uk_:
merged
Changeset 69720:be6634e99e09 by angeliki koutsoukouargyraki _ak2110@cam.ac.uk_:
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
Changeset 69719:331ef175a112 by wenzelm:
Backed out changeset 1bc422c08209 -- obsolete in AFP/5d11846ac6ab;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 69718:f7f3ed2eea0a by blanchet:
really keep lambdas in translation if only predicates are missing
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
Changeset 69717:eb74ff534b27 by blanchet:
tune ATP settings
The file was modified src/HOL/Tools/ATP/atp_problem.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 69716:749aaeb40788 by manuel eberl _eberlm@in.tum.de_:
Added triangular numbers
The file was addedsrc/HOL/ex/Triangular_Numbers.thy
The file was modified src/HOL/ROOT (diff)
Changeset 69715:1bc422c08209 by wenzelm:
keep Local_Theory.reset for now -- still required in many AFP sessions (amending 1c201e4792cb);
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 69714:b7e708ba7786 by wenzelm:
merged
Changeset 69713:81ca77cb7c8c by wenzelm:
use polyml-test-0a6ebca445fc by default: already quite stable;
The file was modified Admin/components/main (diff)
Changeset 69712:dc85b5b3a532 by paulson _lp15@cam.ac.uk_:
renamings and new material
The file was modified src/HOL/Algebra/Complete_Lattice.thy (diff)
The file was modified src/HOL/Algebra/Group_Action.thy (diff)
The file was modified src/HOL/Algebra/Ideal.thy (diff)
The file was modified src/HOL/Algebra/Polynomials.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Caratheodory.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.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/Elementary_Normed_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Integral_Substitution.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Cardinals/Cardinal_Order_Relation.thy (diff)
The file was modified src/HOL/Cardinals/Ordinal_Arithmetic.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Extension.thy (diff)
The file was modified src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy (diff)
The file was modified src/HOL/IMP/Abs_Int2.thy (diff)
The file was modified src/HOL/IMP/Collecting.thy (diff)
The file was modified src/HOL/IMP/Live.thy (diff)
The file was modified src/HOL/IMP/Live_True.thy (diff)
The file was modified src/HOL/Library/Countable_Set_Type.thy (diff)
The file was modified src/HOL/Library/Disjoint_Sets.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Metis_Examples/Abstraction.thy (diff)
The file was modified src/HOL/Metis_Examples/Big_O.thy (diff)
The file was modified src/HOL/Metis_Examples/Message.thy (diff)
The file was modified src/HOL/Probability/Conditional_Expectation.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
The file was modified src/HOL/Probability/Projective_Limit.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy (diff)
The file was modified src/HOL/Vector_Spaces.thy (diff)
Changeset 69711:82a604715919 by paulson:
merged
Changeset 69710:61372780515b by paulson _lp15@cam.ac.uk_:
some renamings and a bit of new material
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Infinite_Set_Sum.thy (diff)
The file was modified src/HOL/Library/FuncSet.thy (diff)
The file was modified src/HOL/Probability/Weak_Convergence.thy (diff)
Changeset 69709:7263b59219c1 by haftmann:
slightly more conventional naming schema
The file was modified NEWS (diff)
The file was modified src/HOL/Tools/Function/function_core.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/inductive_set.ML (diff)
Changeset 69708:1c201e4792cb by haftmann:
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
The file was modified NEWS (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)