Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust: proper transfer if Context.eq_thy_id;
  2. merged
  3. tuned;
  4. tuned;
  5. more robust hg_url; clarified signature;
  6. proper usage (amending 8c7706b053c7);
  7. proper escape for literal single quotes;
  8. some uses of "' " as witness for this feature;
  9. allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
  10. tidied up a few little proofs
Changeset 71553:cf2406e654cf by wenzelm:
more robust: proper transfer if Context.eq_thy_id;
The file was modified src/Pure/thm.ML (diff)
Changeset 71552:309eeea0b2c6 by wenzelm:
merged
Changeset 71551:76ec3baeec9d by wenzelm:
tuned;
The file was modified NEWS (diff)
Changeset 71550:f2b944898636 by wenzelm:
tuned;
The file was modified src/Pure/Tools/phabricator.scala (diff)
Changeset 71549:319599ba28cf by wenzelm:
more robust hg_url;<br>clarified signature;
The file was modified src/Pure/General/ssh.scala (diff)
Changeset 71548:e32255318cb2 by wenzelm:
proper usage (amending 8c7706b053c7);
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
Changeset 71547:d350aabace23 by wenzelm:
proper escape for literal single quotes;
The file was modified NEWS (diff)
The file was modified src/HOL/Bali/DeclConcepts.thy (diff)
The file was modified src/HOL/MicroJava/BV/JVMType.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
Changeset 71546:4dd5dadfc87d by wenzelm:
some uses of &quot;&#039; &quot; as witness for this feature;
The file was modified src/Doc/Classes/Setup.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/Pure/pure_thy.ML (diff)
The file was modified src/ZF/Bin.thy (diff)
Changeset 71545:b0b16088ccf2 by wenzelm:
allow slightly odd &quot;&#039; &quot; in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
The file was modified NEWS (diff)
The file was modified src/Pure/Syntax/syntax_ext.ML (diff)
Changeset 71544:66bc4b668d6e by paulson _lp15@cam.ac.uk_:
tidied up a few little proofs
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Wellfounded.thy (diff)
The file was modified src/HOL/Wfrec.thy (diff)