remove Barrier(MFENCE), remove some comments, change Flush to FlushOne
move some unused materials about hoare logic to hoare.v
defines "data-race"
defines "data-race-free"
correct one error of semantics of Lock/Unlock
add event to astep/bstep; use tactic to speed up deterministic proofs of astep/bstep
add "event" in state's small-step semantics
add "trace" to configuration
let writes/reads depend on events; redefine stuck of state
add SC semantics
try defining DRF Property
change name to st_normal_form & cfg_normal_form
Merge branch 'drf' into dev

Conflicts:
	tso.v
trace is also appending to the end
add axioms in classical logic; add append() for write() and add_event()
update definition for data_race in SC
state required theorems in plain words
now have EV_None; each cfg smallstep also return t*evt, multistep collects them into a trace
stated and started proving diamon theorem, but it's too long, save for later
start defining "flattening"