Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. moved most material from session HOL-Word to Word_Lib in the AFP
  2. removed dependency
Changeset 72515:c7038c397ae3 by haftmann:
moved most material from session HOL-Word to Word_Lib in the AFP
The file was addedsrc/HOL/Library/Tools/smt_word.ML
The file was addedsrc/HOL/Library/Tools/word_lib.ML
The file was addedsrc/HOL/Library/Word.thy
The file was modified NEWS (diff)
The file was modified src/Doc/System/Server.thy (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/HOL/Codegenerator_Test/Candidates.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/SMT_Examples/SMT_Word_Examples.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy (diff)
The file was modified src/HOL/SPARK/SPARK_Setup.thy (diff)
The file was modified src/HOL/ex/Bit_Lists.thy (diff)
The file was removedsrc/HOL/Word/Ancient_Numeral.thy
The file was removedsrc/HOL/Word/Bit_Comprehension.thy
The file was removedsrc/HOL/Word/Misc_Arithmetic.thy
The file was removedsrc/HOL/Word/Misc_Auxiliary.thy
The file was removedsrc/HOL/Word/Misc_Typedef.thy
The file was removedsrc/HOL/Word/Misc_lsb.thy
The file was removedsrc/HOL/Word/Misc_msb.thy
The file was removedsrc/HOL/Word/Misc_set_bit.thy
The file was removedsrc/HOL/Word/More_Word.thy
The file was removedsrc/HOL/Word/Reversed_Bit_Lists.thy
The file was removedsrc/HOL/Word/Tools/smt_word.ML
The file was removedsrc/HOL/Word/Tools/word_lib.ML
The file was removedsrc/HOL/Word/Word.thy
The file was removedsrc/HOL/Word/Word_Examples.thy
The file was removedsrc/HOL/Word/Word_rsplit.thy
The file was removedsrc/HOL/Word/document/root.bib
The file was removedsrc/HOL/Word/document/root.tex
Changeset 72514:d8661799afb2 by haftmann:
removed dependency
The file was modified src/HOL/SMT_Examples/SMT_Word_Examples.thy (diff)
The file was modified src/HOL/SPARK/Manual/Reference.thy (diff)
The file was modified src/HOL/Word/Tools/smt_word.ML (diff)
The file was modified src/HOL/Word/Traditional_Syntax.thy (diff)