Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. resolved conflict
  3. more canonical names
  4. more canonical names
  5. more canonical names
  6. merged
  7. merged;
  8. support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
  9. avoid outdated Process.interruptConsoleProcesses;
  10. tuning
  11. updated doc
  12. tuning
  13. Merge
  14. New and revised material for (multivariate) analysis
Changeset 62394:d71774989c4a by nipkow:
merged
Changeset 62393:a620a8756b7c by nipkow:
resolved conflict
Changeset 62392:747d36865c2c by nipkow:
more canonical names
The file was modified src/Doc/Isar_Ref/Generic.thy (diff)
The file was modified src/Doc/Tutorial/Fun/fun0.thy (diff)
The file was modified src/Doc/Tutorial/Misc/simp.thy (diff)
The file was modified src/Doc/Tutorial/Protocol/Event.thy (diff)
The file was modified src/Doc/Tutorial/Protocol/Message.thy (diff)
The file was modified src/Doc/Tutorial/Protocol/Public.thy (diff)
The file was modified src/Doc/Tutorial/Recdef/simplification.thy (diff)
The file was modified src/Doc/Tutorial/Types/Setup.thy (diff)
Changeset 62391:1658fc9b2618 by nipkow:
more canonical names
The file was modified src/HOL/Decision_Procs/approximation.ML (diff)
The file was modified src/HOL/Decision_Procs/langford.ML (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/report.ML (diff)
The file was modified src/HOL/Statespace/distinct_tree_prover.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/core_data.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/mode_inference.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/abstract_generators.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was modified src/HOL/Tools/boolean_algebra_cancel.ML (diff)
Changeset 62390:842917225d56 by nipkow:
more canonical names
The file was modified src/HOL/Auth/Guard/Extensions.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard.thy (diff)
The file was modified src/HOL/Auth/Guard/GuardK.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_Shared.thy (diff)
The file was modified src/HOL/Auth/Guard/P1.thy (diff)
The file was modified src/HOL/Auth/Guard/P2.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/BNF_Cardinal_Order_Relation.thy (diff)
The file was modified src/HOL/Bali/AxCompl.thy (diff)
The file was modified src/HOL/Bali/AxExample.thy (diff)
The file was modified src/HOL/Bali/AxSem.thy (diff)
The file was modified src/HOL/Bali/AxSound.thy (diff)
The file was modified src/HOL/Bali/Basis.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/Example.thy (diff)
The file was modified src/HOL/Bali/State.thy (diff)
The file was modified src/HOL/Bali/Term.thy (diff)
The file was modified src/HOL/Bali/Trans.thy (diff)
The file was modified src/HOL/Bali/TypeSafe.thy (diff)
The file was modified src/HOL/Bali/WellForm.thy (diff)
The file was modified src/HOL/Bali/WellType.thy (diff)
The file was modified src/HOL/Cardinals/Cardinal_Arithmetic.thy (diff)
The file was modified src/HOL/Cardinals/Ordinal_Arithmetic.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Data_Structures/AA_Set.thy (diff)
The file was modified src/HOL/Data_Structures/Isin2.thy (diff)
The file was modified src/HOL/Data_Structures/Lookup2.thy (diff)
The file was modified src/HOL/Data_Structures/Tree2.thy (diff)
The file was modified src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/Decision_Procs/Polynomial_List.thy (diff)
The file was modified src/HOL/Decision_Procs/Rat_Pair.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Divides.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/HOL.thy (diff)
The file was modified src/HOL/HOLCF/Bifinite.thy (diff)
The file was modified src/HOL/HOLCF/IOA/ABP/Correctness.thy (diff)
The file was modified src/HOL/HOLCF/IOA/Deadlock.thy (diff)
The file was modified src/HOL/HOLCF/IOA/NTP/Correctness.thy (diff)
The file was modified src/HOL/HOLCF/IOA/NTP/Impl.thy (diff)
The file was modified src/HOL/HOLCF/IOA/RefCorrectness.thy (diff)
The file was modified src/HOL/HOLCF/IOA/RefMappings.thy (diff)
The file was modified src/HOL/HOLCF/IOA/SimCorrectness.thy (diff)
The file was modified src/HOL/HOLCF/IOA/TL.thy (diff)
The file was modified src/HOL/HOLCF/IOA/TLS.thy (diff)
The file was modified src/HOL/HOLCF/Universal.thy (diff)
The file was modified src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy (diff)
The file was modified src/HOL/Hoare/Examples.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Com.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Hoare.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Syntax.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Tran.thy (diff)
The file was modified src/HOL/Hoare_Parallel/Quote_Antiquote.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Com.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Syntax.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Tran.thy (diff)
The file was modified src/HOL/IMP/Compiler2.thy (diff)
The file was modified src/HOL/IMP/Finite_Reachable.thy (diff)
The file was modified src/HOL/IOA/Solve.thy (diff)
The file was modified src/HOL/Imperative_HOL/Overview.thy (diff)
The file was modified src/HOL/Imperative_HOL/ex/Sorted_List.thy (diff)
The file was modified src/HOL/Imperative_HOL/ex/Subarray.thy (diff)
The file was modified src/HOL/Induct/Common_Patterns.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Isar_Examples/Group.thy (diff)
The file was modified src/HOL/Library/AList.thy (diff)
The file was modified src/HOL/Library/Bourbaki_Witt_Fixpoint.thy (diff)
The file was modified src/HOL/Library/Cardinality.thy (diff)
The file was modified src/HOL/Library/Countable_Complete_Lattices.thy (diff)
The file was modified src/HOL/Library/Countable_Set.thy (diff)
The file was modified src/HOL/Library/Countable_Set_Type.thy (diff)
The file was modified src/HOL/Library/Discrete.thy (diff)
The file was modified src/HOL/Library/Disjoint_Sets.thy (diff)
The file was modified src/HOL/Library/Dlist.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Library/FinFun.thy (diff)
The file was modified src/HOL/Library/FinFun_Syntax.thy (diff)
The file was modified src/HOL/Library/Float.thy (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/FuncSet.thy (diff)
The file was modified src/HOL/Library/Indicator_Function.thy (diff)
The file was modified src/HOL/Library/Lattice_Constructions.thy (diff)
The file was modified src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Nonpos_Ints.thy (diff)
The file was modified src/HOL/Library/Periodic_Fun.thy (diff)
The file was modified src/HOL/Library/Permutations.thy (diff)
The file was modified src/HOL/Library/RBT_Impl.thy (diff)
The file was modified src/HOL/Library/RBT_Mapping.thy (diff)
The file was modified src/HOL/Library/Transitive_Closure_Table.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Map.thy (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy (diff)
The file was modified src/HOL/Matrix_LP/LP.thy (diff)
The file was modified src/HOL/Matrix_LP/Matrix.thy (diff)
The file was modified src/HOL/Metis_Examples/Message.thy (diff)
The file was modified src/HOL/Metis_Examples/Tarski.thy (diff)
The file was modified src/HOL/MicroJava/BV/BVSpecTypeSafe.thy (diff)
The file was modified src/HOL/MicroJava/BV/Effect.thy (diff)
The file was modified src/HOL/MicroJava/BV/JType.thy (diff)
The file was modified src/HOL/MicroJava/Comp/AuxLemmas.thy (diff)
The file was modified src/HOL/MicroJava/Comp/CorrCompTp.thy (diff)
The file was modified src/HOL/MicroJava/DFA/Abstract_BV.thy (diff)
The file was modified src/HOL/MicroJava/DFA/LBVComplete.thy (diff)
The file was modified src/HOL/MicroJava/DFA/LBVCorrect.thy (diff)
The file was modified src/HOL/MicroJava/DFA/LBVSpec.thy (diff)
The file was modified src/HOL/MicroJava/DFA/Semilattices.thy (diff)
The file was modified src/HOL/MicroJava/DFA/Typing_Framework_err.thy (diff)
The file was modified src/HOL/MicroJava/J/Example.thy (diff)
The file was modified src/HOL/MicroJava/J/Exceptions.thy (diff)
The file was modified src/HOL/MicroJava/J/JTypeSafe.thy (diff)
The file was modified src/HOL/MicroJava/J/State.thy (diff)
The file was modified src/HOL/MicroJava/J/TypeRel.thy (diff)
The file was modified src/HOL/MicroJava/J/WellForm.thy (diff)
The file was modified src/HOL/MicroJava/J/WellType.thy (diff)
The file was modified src/HOL/MicroJava/JVM/JVMDefensive.thy (diff)
The file was modified src/HOL/MicroJava/JVM/JVMExceptions.thy (diff)
The file was modified src/HOL/MicroJava/JVM/JVMExecInstr.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Derivative.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Gamma.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Integral_Test.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Integration.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/ex/Approximations.thy (diff)
The file was modified src/HOL/NSA/HyperDef.thy (diff)
The file was modified src/HOL/NanoJava/OpSem.thy (diff)
The file was modified src/HOL/NanoJava/TypeRel.thy (diff)
The file was modified src/HOL/Nominal/Examples/Compile.thy (diff)
The file was modified src/HOL/Nominal/Examples/Pattern.thy (diff)
The file was modified src/HOL/Nominal/Examples/SN.thy (diff)
The file was modified src/HOL/Nominal/Examples/Standardization.thy (diff)
The file was modified src/HOL/Nominal/Examples/Support.thy (diff)
The file was modified src/HOL/Nominal/Examples/VC_Condition.thy (diff)
The file was modified src/HOL/Nominal/Examples/Weakening.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Partial_Function.thy (diff)
The file was modified src/HOL/Predicate.thy (diff)
The file was modified src/HOL/Predicate_Compile.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Hotel_Example.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/List_Examples.thy (diff)
The file was modified src/HOL/Probability/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Probability/Bochner_Integration.thy (diff)
The file was modified src/HOL/Probability/Borel_Space.thy (diff)
The file was modified src/HOL/Probability/Caratheodory.thy (diff)
The file was modified src/HOL/Probability/Complete_Measure.thy (diff)
The file was modified src/HOL/Probability/Discrete_Topology.thy (diff)
The file was modified src/HOL/Probability/Distributions.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
The file was modified src/HOL/Probability/Finite_Product_Measure.thy (diff)
The file was modified src/HOL/Probability/Independent_Family.thy (diff)
The file was modified src/HOL/Probability/Infinite_Product_Measure.thy (diff)
The file was modified src/HOL/Probability/Information.thy (diff)
The file was modified src/HOL/Probability/Interval_Integral.thy (diff)
The file was modified src/HOL/Probability/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Probability/Measurable.thy (diff)
The file was modified src/HOL/Probability/Measure_Space.thy (diff)
The file was modified src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Probability/Probability_Mass_Function.thy (diff)
The file was modified src/HOL/Probability/Probability_Measure.thy (diff)
The file was modified src/HOL/Probability/Radon_Nikodym.thy (diff)
The file was modified src/HOL/Probability/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Probability/Sinc_Integral.thy (diff)
The file was modified src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy (diff)
The file was modified src/HOL/Probability/ex/Measure_Not_CCC.thy (diff)
The file was modified src/HOL/Proofs/Lambda/ListBeta.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
The file was modified src/HOL/SET_Protocol/Message_SET.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Statespace/DistinctTreeProver.thy (diff)
The file was modified src/HOL/Statespace/StateFun.thy (diff)
The file was modified src/HOL/Statespace/StateSpaceLocale.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Interpret.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Interpret_Test.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Parser.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Parser_Test.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Test.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
The file was modified src/HOL/UNITY/Lift_prog.thy (diff)
The file was modified src/HOL/UNITY/Simple/Channel.thy (diff)
The file was modified src/HOL/UNITY/Simple/Lift.thy (diff)
The file was modified src/HOL/UNITY/Simple/Reach.thy (diff)
The file was modified src/HOL/UNITY/Simple/Reachability.thy (diff)
The file was modified src/HOL/Word/Bool_List_Representation.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was modified src/HOL/Word/WordBitwise.thy (diff)
The file was modified src/HOL/Word/Word_Miscellaneous.thy (diff)
The file was modified src/HOL/ex/Cubic_Quartic.thy (diff)
The file was modified src/HOL/ex/Erdoes_Szekeres.thy (diff)
The file was modified src/HOL/ex/FinFunPred.thy (diff)
The file was modified src/HOL/ex/Induction_Schema.thy (diff)
The file was modified src/HOL/ex/Pythagoras.thy (diff)
The file was modified src/HOL/ex/Tarski.thy (diff)
The file was modified src/HOL/ex/Unification.thy (diff)
The file was modified src/HOL/ex/While_Combinator_Example.thy (diff)
Changeset 62389:07bfd581495d by wenzelm:
merged
Changeset 62388:274f279c09e9 by wenzelm:
merged;
Changeset 62387:ad3eb2889f9a by wenzelm:
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
The file was addedsrc/Pure/RAW/fixed_int_dummy.ML
The file was modified Admin/polyml/build (diff)
The file was modified src/Pure/General/pretty.ML (diff)
The file was modified src/Pure/ML/exn_output.ML (diff)
The file was modified src/Pure/ML/exn_properties.ML (diff)
The file was modified src/Pure/ML/install_pp_polyml.ML (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/RAW/ROOT_polyml.ML (diff)
The file was modified src/Pure/RAW/compiler_polyml.ML (diff)
The file was modified src/Pure/RAW/ml_debugger_polyml-5.6.ML (diff)
The file was modified src/Pure/RAW/ml_pretty.ML (diff)
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/Tools/debugger.ML (diff)
Changeset 62386:10e55e168672 by wenzelm:
avoid outdated Process.interruptConsoleProcesses;
The file was modified lib/scripts/run-polyml-5.6 (diff)
Changeset 62385:7891843d79bb by blanchet:
tuning
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
Changeset 62384:54512bd12a5e by blanchet:
updated doc
The file was modified src/Doc/Datatypes/Datatypes.thy (diff)
Changeset 62383:f60085077ab0 by blanchet:
tuning
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
Changeset 62382:ff5d7a9831ef by paulson _lp15@cam.ac.uk_:
Merge
Changeset 62381:a6479cb85944 by paulson _lp15@cam.ac.uk_:
New and revised material for (multivariate) analysis
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Meson.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Derivative.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Summation.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Series.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)