Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. parse logical operators in the right order w.r.t. backtracking
  2. improved warning
  3. adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing)
  4. operations for symbolic computation of bit operations
  5. proper local context
Changeset 73972:b304285fd800 by blanchet:
parse logical operators in the right order w.r.t. backtracking
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
Changeset 73971:96a05b8462f9 by blanchet:
improved warning
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
Changeset 73970:34c8cf767fa3 by blanchet:
adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing)
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 73969:ca2a35c0fe6e by haftmann:
operations for symbolic computation of bit operations
The file was modified src/HOL/Library/Bit_Operations.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
Changeset 73968:0274d442b7ea by haftmann:
proper local context
The file was modified src/HOL/Library/RBT_Set.thy (diff)
The file was modified src/Pure/Isar/code.ML (diff)