Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. List_Lexorder finally working
  2. lexicographic ordering: new simp setup to prioritise the simpler "less_than" case
  3. merged
  4. fixed for new lex-order. And the effing indentation!
  5. merged
  6. S Holub's proposed generalisation of the lexicographic product of two orderings
Changeset 72169:2d7619fc0e1a by paulson _lp15@cam.ac.uk_:
List_Lexorder finally working
The file was modified src/HOL/Library/List_Lexorder.thy (diff)
Changeset 72168:721a05da8fe7 by paulson _lp15@cam.ac.uk_:
lexicographic ordering: new simp setup to prioritise the simpler "less_than" case
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 72167:e5765cfd4338 by paulson:
merged
Changeset 72166:bb37571139bf by paulson _lp15@cam.ac.uk_:
fixed for new lex-order. And the effing indentation!
The file was modified src/HOL/Library/List_Lexorder.thy (diff)
The file was modified src/HOL/Nominal/Examples/Class3.thy (diff)
Changeset 72165:605f151585e0 by paulson:
merged
Changeset 72164:b7c54ff7f2dd by paulson _lp15@cam.ac.uk_:
S Holub's proposed generalisation of the lexicographic product of two orderings
The file was modified src/HOL/Fun_Def.thy (diff)
The file was modified src/HOL/Library/List_Lenlexorder.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/String.thy (diff)
The file was modified src/HOL/Wellfounded.thy (diff)