Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. back to scala-2.12.2, after a41435469559;
  2. more direct construction of integer_of_num; code equations for integer_of_char may rely on pattern matching on Char
  3. treat "undefined" constants internally as special form of case combinators
  4. Improved error reporting when activating a locale instance (beyond syntax decls).
  5. Additional corollary Knaster_Tarski_idem_inf_eq.
  6. clarified indentation;
  7. clarified indentation;
Changeset 66191:d91108ba9474 by wenzelm:
back to scala-2.12.2, after a41435469559;
The file was modified Admin/components/main (diff)
The file was modified src/HOL/Codegenerator_Test/Generate.thy (diff)
The file was modified src/Pure/General/antiquote.scala (diff)
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/timing_dockable.scala (diff)
Changeset 66190:a41435469559 by haftmann:
more direct construction of integer_of_num;<br>code equations for integer_of_char may rely on pattern matching on Char
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Library/Code_Target_Nat.thy (diff)
The file was modified src/HOL/String.thy (diff)
Changeset 66189:23917e861eaa by haftmann:
treat &quot;undefined&quot; constants internally as special form of case combinators
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 66188:bd841164592f by ballarin:
Improved error reporting when activating a locale instance (beyond syntax decls).
The file was modified src/Pure/Isar/locale.ML (diff)
Changeset 66187:85925d4ae93d by ballarin:
Additional corollary Knaster_Tarski_idem_inf_eq.
The file was modified src/HOL/Algebra/Complete_Lattice.thy (diff)
Changeset 66186:9de577f2dc3b by wenzelm:
clarified indentation;
The file was modified src/Tools/jEdit/src/completion_popup.scala (diff)
Changeset 66185:aa002ed3f6d1 by wenzelm:
clarified indentation;
The file was modified src/Tools/jEdit/src/completion_popup.scala (diff)