Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tunin
  2. tuning
  3. added lemmas
  4. added omega notation (+ improved ROOT file)
  5. use abbreviation for omega
Changeset 7702:79d51e806974 by blanchet:
tunin
The file was modified thys/Nested_Multisets_Ordinals/Goodstein_Sequence.thy (diff)
Changeset 7701:c05a6cfd853e by blanchet:
tuning
The file was modified thys/Nested_Multisets_Ordinals/Goodstein_Sequence.thy (diff)
Changeset 7700:97a4eb28ed82 by blanchet:
added lemmas
The file was modified thys/Nested_Multisets_Ordinals/Hydra_Battle.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Syntactic_Ordinal.thy (diff)
Changeset 7699:b4992a3c610d by blanchet:
added omega notation (+ improved ROOT file)
The file was modified thys/Nested_Multisets_Ordinals/Goodstein_Sequence.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Hydra_Battle.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Multiset_More.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/ROOT (diff)
The file was modified thys/Nested_Multisets_Ordinals/Signed_Syntactic_Ordinal.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Syntactic_Ordinal.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Syntactic_Ordinal_Bridge.thy (diff)
Changeset 7698:ed5d5755367c by blanchet:
use abbreviation for omega
The file was modified thys/Nested_Multisets_Ordinals/Signed_Syntactic_Ordinal.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Syntactic_Ordinal.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Syntactic_Ordinal_Bridge.thy (diff)