Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. still not quite fixed...
  3. A few more reversions
  4. reversion to the explicit existential quantifier
  5. more tidying of messy proofs
  6. clarified signature;
  7. clarified signature;
  8. clarified signature;
  9. clarified signature;
Changeset 72383:698b58513fd1 by paulson:
merged
Changeset 72382:6cacbdb53637 by paulson _lp15@cam.ac.uk_:
still not quite fixed...
The file was modified src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Complex_Analysis/Winding_Numbers.thy (diff)
Changeset 72381:15ea20d8a4d6 by paulson _lp15@cam.ac.uk_:
A few more reversions
The file was modified src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Complex_Analysis/Winding_Numbers.thy (diff)
Changeset 72380:becf08cb81e1 by paulson _lp15@cam.ac.uk_:
reversion to the explicit existential quantifier
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
Changeset 72379:504fe7365820 by paulson _lp15@cam.ac.uk_:
more tidying of messy proofs
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy (diff)
The file was modified src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Complex_Analysis/Winding_Numbers.thy (diff)
Changeset 72378:075f3cbc7546 by wenzelm:
clarified signature;
The file was modified src/Pure/Admin/build_e.scala (diff)
The file was modified src/Pure/Admin/build_polyml.scala (diff)
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/General/file.scala (diff)
Changeset 72377:c7741f767e3e by wenzelm:
clarified signature;
The file was modified src/Pure/Admin/build_e.scala (diff)
The file was modified src/Pure/Admin/build_polyml.scala (diff)
The file was modified src/Pure/Admin/build_sqlite.scala (diff)
The file was modified src/Pure/System/isabelle_system.scala (diff)
Changeset 72376:04bce3478688 by wenzelm:
clarified signature;
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/Pure/Admin/build_cygwin.scala (diff)
The file was modified src/Pure/Admin/build_e.scala (diff)
The file was modified src/Pure/Admin/build_fonts.scala (diff)
The file was modified src/Pure/Admin/build_jdk.scala (diff)
The file was modified src/Pure/Admin/build_polyml.scala (diff)
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/Admin/build_sqlite.scala (diff)
The file was modified src/Pure/Admin/build_status.scala (diff)
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
The file was modified src/Pure/General/ssh.scala (diff)
The file was modified src/Pure/System/isabelle_system.ML (diff)
The file was modified src/Pure/System/isabelle_system.scala (diff)
The file was modified src/Pure/Thy/html.scala (diff)
The file was modified src/Pure/Thy/present.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/phabricator.scala (diff)
The file was modified src/Pure/Tools/scala_project.scala (diff)
Changeset 72375:e48d93811ed7 by wenzelm:
clarified signature;
The file was modified src/Doc/Codegen/Evaluation.thy (diff)
The file was modified src/Doc/Codegen/Introduction.thy (diff)
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/Pure/Admin/build_cygwin.scala (diff)
The file was modified src/Pure/Admin/build_e.scala (diff)
The file was modified src/Pure/Admin/build_fonts.scala (diff)
The file was modified src/Pure/Admin/build_history.scala (diff)
The file was modified src/Pure/Admin/build_jdk.scala (diff)
The file was modified src/Pure/Admin/build_log.scala (diff)
The file was modified src/Pure/Admin/build_polyml.scala (diff)
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/Admin/build_sqlite.scala (diff)
The file was modified src/Pure/Admin/build_status.scala (diff)
The file was modified src/Pure/Admin/components.scala (diff)
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
The file was modified src/Pure/Admin/jenkins.scala (diff)
The file was modified src/Pure/Admin/other_isabelle.scala (diff)
The file was modified src/Pure/General/completion.scala (diff)
The file was modified src/Pure/General/mercurial.scala (diff)
The file was modified src/Pure/General/ssh.scala (diff)
The file was modified src/Pure/System/isabelle_system.ML (diff)
The file was modified src/Pure/System/isabelle_system.scala (diff)
The file was modified src/Pure/System/options.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/html.scala (diff)
The file was modified src/Pure/Thy/present.ML (diff)
The file was modified src/Pure/Thy/present.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
The file was modified src/Pure/Tools/generated_files.ML (diff)
The file was modified src/Pure/Tools/main.scala (diff)
The file was modified src/Pure/Tools/mkroot.scala (diff)
The file was modified src/Pure/Tools/phabricator.scala (diff)
The file was modified src/Pure/Tools/scala_project.scala (diff)
The file was modified src/Pure/Tools/spell_checker.scala (diff)
The file was modified src/Tools/Code/code_target.ML (diff)