Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more direct construction of integer_of_num; code equations for integer_of_char may rely on pattern matching on Char
  2. treat "undefined" constants internally as special form of case combinators
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)