Changes

Summary

model characters directly as range 0..255 * * * operate on syntax terms rather than asts

Changeset 62597:b3f2b8c906a6 by haftmann: model characters directly as range 0..255<br>* * *<br>operate on syntax terms rather than asts
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Code_Evaluation.thy` (diff)
The file was modified	`src/HOL/Divides.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Char_Discrete.thy` (diff)
The file was modified	`src/HOL/Library/Cardinality.thy` (diff)
The file was modified	`src/HOL/Library/Char_ord.thy` (diff)
The file was modified	`src/HOL/Library/Code_Char.thy` (diff)
The file was modified	`src/HOL/Library/Code_Test.thy` (diff)
The file was modified	`src/HOL/Library/Predicate_Compile_Alternative_Defs.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Datatype_Nits.thy` (diff)
The file was modified	`src/HOL/Num.thy` (diff)
The file was modified	`src/HOL/Parity.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Exhaustive.thy` (diff)
The file was modified	`src/HOL/Statespace/state_fun.ML` (diff)
The file was modified	`src/HOL/String.thy` (diff)
The file was modified	`src/HOL/Tools/hologic.ML` (diff)
The file was modified	`src/HOL/Tools/numeral.ML` (diff)
The file was modified	`src/HOL/Tools/string_code.ML` (diff)
The file was modified	`src/HOL/Tools/string_syntax.ML` (diff)
The file was modified	`src/HOL/ex/Cartouche_Examples.thy` (diff)