Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. unfolding set_lebesgue_integral_def
  2. unfolding set_integrable_def, etc
  3. unfolding set_lebesgue_integral_def, etc.
  4. unfolding set_lebesgue_integral_def, etc.
  5. fixed for new dominated_convergence
  6. merged
  7. merged
  8. merged
  9. specialize some local functions
  10. fix bad simplifier context warnings
  11. remove trailing whitespace
  12. merge
  13. slight change
  14. improved efficiency of implementation of LLL by using dedicated ^2 operation on rational numbers
  15. Markov_Models now working with set_lebesgue_integral_def, etc.
Changeset 9095:365208ad4472 by paulson _lp15@cam.ac.uk_:
unfolding set_lebesgue_integral_def
The file was modified thys/Buffons_Needle/Buffons_Needle.thy (diff)
Changeset 9094:946b7993385e by paulson _lp15@cam.ac.uk_:
unfolding set_integrable_def, etc
The file was modified thys/Error_Function/Error_Function.thy (diff)
Changeset 9093:07f4d31f43c0 by paulson _lp15@cam.ac.uk_:
unfolding set_lebesgue_integral_def, etc.
The file was modified thys/Ergodic_Theory/Invariants.thy (diff)
The file was modified thys/Ergodic_Theory/Recurrence.thy (diff)
The file was modified thys/Ergodic_Theory/SG_Library_Complement.thy (diff)
The file was modified thys/Ergodic_Theory/Transfer_Operator.thy (diff)
Changeset 9092:30f7922d6d17 by paulson _lp15@cam.ac.uk_:
unfolding set_lebesgue_integral_def, etc.
The file was modified thys/Zeta_Function/Zeta_Function.thy (diff)
Changeset 9091:055cf8c4277f by paulson _lp15@cam.ac.uk_:
fixed for new dominated_convergence
The file was modified thys/Stirling_Formula/Stirling_Formula.thy (diff)
Changeset 9090:0920eac9b47a by huffman:
merged
Changeset 9089:c528c3e3a691 by huffman:
merged
Changeset 9088:df4a086e0e3e by huffman:
merged
Changeset 9087:da745398907d by huffman:
specialize some local functions
The file was modified thys/Nominal2/nominal_dt_rawfuns.ML (diff)
Changeset 9086:fbd3355d6351 by huffman:
fix bad simplifier context warnings
The file was modified thys/Nominal2/nominal_eqvt.ML (diff)
Changeset 9085:4ef8cdcfd257 by huffman:
remove trailing whitespace
The file was modified thys/Nominal2/Eqvt.thy (diff)
The file was modified thys/Nominal2/Nominal2.thy (diff)
The file was modified thys/Nominal2/Nominal2_Abs.thy (diff)
The file was modified thys/Nominal2/Nominal2_Base.thy (diff)
The file was modified thys/Nominal2/Nominal2_FCB.thy (diff)
The file was modified thys/Nominal2/nominal_atoms.ML (diff)
The file was modified thys/Nominal2/nominal_basics.ML (diff)
The file was modified thys/Nominal2/nominal_dt_alpha.ML (diff)
The file was modified thys/Nominal2/nominal_dt_data.ML (diff)
The file was modified thys/Nominal2/nominal_dt_quot.ML (diff)
The file was modified thys/Nominal2/nominal_dt_rawfuns.ML (diff)
The file was modified thys/Nominal2/nominal_eqvt.ML (diff)
The file was modified thys/Nominal2/nominal_function.ML (diff)
The file was modified thys/Nominal2/nominal_function_common.ML (diff)
The file was modified thys/Nominal2/nominal_function_core.ML (diff)
The file was modified thys/Nominal2/nominal_induct.ML (diff)
The file was modified thys/Nominal2/nominal_inductive.ML (diff)
The file was modified thys/Nominal2/nominal_library.ML (diff)
The file was modified thys/Nominal2/nominal_mutual.ML (diff)
The file was modified thys/Nominal2/nominal_permeq.ML (diff)
The file was modified thys/Nominal2/nominal_termination.ML (diff)
Changeset 9084:f4a0575727e0 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge
Changeset 9083:ba83fa7cd1c9 by rene thiemann _rene.thiemann@uibk.ac.at_:
slight change
The file was modified thys/LLL_Basis_Reduction/LLL_Complexity.thy (diff)
Changeset 9082:db25d75303d9 by rene thiemann _rene.thiemann@uibk.ac.at_:
improved efficiency of implementation of LLL by using dedicated ^2 operation on rational numbers
The file was modified thys/LLL_Basis_Reduction/Gram_Schmidt_2.thy (diff)
The file was modified thys/LLL_Basis_Reduction/LLL.thy (diff)
The file was modified thys/LLL_Basis_Reduction/LLL_Complexity.thy (diff)
Changeset 9081:d2a7c5bce332 by paulson _lp15@cam.ac.uk_:
Markov_Models now working with set_lebesgue_integral_def, etc.
The file was modified thys/Markov_Models/Continuous_Time_Markov_Chain.thy (diff)