Skip to content
Success

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier;
  2. more concise instance-specific rules on euclidean relation
  3. merged
  4. Tidied a few more proofs
  5. merged
  6. tidied a few ugly proofs
  7. let rsync re-use ssh connection via control path;
  8. clarified command-line;
  9. clarified command-line;
  10. tuned signature;
  11. proper port for Mercurial;
  12. clarified default: do not override port from ssh_config, which could be different from 22;
  13. proper Scala expression;
  14. clarified signature: separate unrelated modules;
  15. tuned;
Changeset 76142:e8d4013c49d1 by wenzelm:
more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier;
The file was modified src/Pure/General/ssh.scala
Changeset 76141:e7497a1de8b9 by haftmann:
more concise instance-specific rules on euclidean relation
The file was modified src/HOL/Divides.thy
The file was modified src/HOL/Euclidean_Division.thy
Changeset 76140:19837257fd89 by paulson:
merged
Changeset 76139:3190ee65139b by paulson _lp15@cam.ac.uk_:
Tidied a few more proofs
The file was modified src/HOL/Analysis/Polytope.thy
Changeset 76138:02a743911ffe by paulson:
merged
Changeset 76137:175e6d47e3af by paulson _lp15@cam.ac.uk_:
tidied a few ugly proofs
The file was modified src/HOL/Analysis/Complex_Transcendental.thy
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy
Changeset 76136:1bb677cceea4 by wenzelm:
let rsync re-use ssh connection via control path;
The file was modified src/Doc/System/Misc.thy
The file was modified src/Doc/System/Sessions.thy
The file was modified src/Pure/Admin/build_history.scala
The file was modified src/Pure/General/mercurial.scala
The file was modified src/Pure/General/rsync.scala
The file was modified src/Pure/General/ssh.scala
The file was modified src/Pure/Tools/sync.scala
Changeset 76135:a144603170b4 by wenzelm:
clarified command-line;
The file was modified src/Doc/System/Misc.thy
The file was modified src/Doc/System/Sessions.thy
Changeset 76134:c6e0a51f2a93 by wenzelm:
clarified command-line;
The file was modified src/Pure/General/mercurial.scala
The file was modified src/Pure/Tools/sync.scala
Changeset 76133:c5fd7947f585 by wenzelm:
tuned signature;
The file was modified src/Pure/General/ssh.scala
Changeset 76132:2bb6eb6df6c2 by wenzelm:
proper port for Mercurial;
The file was modified src/Pure/General/ssh.scala
Changeset 76131:8b695e59db3f by wenzelm:
clarified default: do not override port from ssh_config, which could be different from 22;
The file was modified src/Doc/System/Misc.thy
The file was modified src/Doc/System/Sessions.thy
The file was modified src/Pure/General/mercurial.scala
The file was modified src/Pure/General/rsync.scala
The file was modified src/Pure/General/ssh.scala
The file was modified src/Pure/Tools/sync.scala
Changeset 76130:b703cecf9bd0 by wenzelm:
proper Scala expression;
The file was modified src/Pure/General/ssh.scala
Changeset 76129:5979f73b9db1 by wenzelm:
clarified signature: separate unrelated modules;
The file was modified src/Pure/Tools/phabricator.scala
Changeset 76128:f5e96a4039a7 by wenzelm:
tuned;
The file was modified src/Pure/General/ssh.scala

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. Purely cosmetic
  3. merged
  4. Deleted one redundant step
  5. merged
  6. Merge
  7. Tidied (a lot)
Changeset 13011:26adfcf755e4 by paulson:
merged
Changeset 13010:4b812a85fec9 by paulson _lp15@cam.ac.uk_:
Purely cosmetic
The file was modified thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy
Changeset 13009:b9a7410ee6a2 by paulson:
merged
Changeset 13008:6bb468a732ea by paulson _lp15@cam.ac.uk_:
Deleted one redundant step
The file was modified thys/Wetzels_Problem/Wetzels_Problem.thy
Changeset 13007:b038dcd37cdc by paulson:
merged
Changeset 13005:50da79b217bc by paulson _lp15@cam.ac.uk_:
Tidied (a lot)
The file was modified thys/Ackermanns_not_PR/Primrec.thy