#
# ChangeLog for src/ASM/StatusProofs.ma
#
# Generated by Trac 1.2
# Mar 4, 2021, 11:10:33 AM

Thu, 02 Aug 2012 11:58:14 GMT sacerdot [2285]
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/ASM/StatusProofsSplit.ma (modified)

	1. duplicated code erased
	2. POP case finished up to lemmas on ...


Fri, 27 Jul 2012 15:53:25 GMT mulligan [2272]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/ASM/StatusProofsSplit.ma (modified)
	* src/ASM/Test.ma (modified)

	Changed proof strategy for main lemma after noticed that the current ...


Tue, 10 Jul 2012 12:39:38 GMT mulligan [2172]
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/ASM/StatusProofsSplit.ma (modified)
	* src/ASM/Test.ma (modified)

	Moved new versions of get_ / set_arg_* into Status.ma.  Commented out ...


Wed, 27 Jun 2012 14:23:54 GMT sacerdot [2124]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)

	Much more shuffling around to proper places


Fri, 08 Jun 2012 14:32:03 GMT sacerdot [2032]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Policy.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/ASM/WellLabeled.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/casts.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/FrontEndVal.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Values.ma (modified)

	!! BEWARE: major commit !!

	1) [affects everybody]
	   split for ...


Wed, 16 May 2012 22:25:41 GMT sacerdot [1962]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/StatusProofs.ma (modified)

	More examples are now indexed.


Wed, 16 May 2012 15:12:22 GMT mulligan [1959]
	* src/ASM/StatusProofs.ma (modified)

	Commented out diverging application of demodulation and closed goals ...


Wed, 16 May 2012 14:47:56 GMT mulligan [1958]
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/StatusProofs.ma (modified)

	Marked divergence in StatusProofs.ma


Mon, 20 Feb 2012 09:04:54 GMT mulligan [1710]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/StatusProofs.ma (modified)

	changes from friday afternoon


Sat, 28 Jan 2012 12:42:15 GMT sacerdot [1666]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)

	PreStatus datatype change: the code_memory field is not a left ...


Wed, 14 Dec 2011 12:40:08 GMT sacerdot [1606]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Interpret2.ma (modified)
	* src/ASM/StatusProofs.ma (modified)

	Porting to last library of Matita.


Tue, 22 Nov 2011 11:37:42 GMT campbell [1530]
	* src/ASM/StatusProofs.ma (modified)

	Update due to Russell changes.


Mon, 21 Nov 2011 11:10:57 GMT campbell [1519]
	* src/ASM/Interpret.ma (modified)
	* src/ASM/StatusProofs.ma (modified)

	More syntax updates.


Fri, 18 Nov 2011 12:03:14 GMT campbell [1515]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Erase.ma (modified)
	* src/ASM/I8051.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Interpret2.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/fresh.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/test/insertsort.test.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (added)
	* src/common/PreIdentifiers.ma (modified)
	* src/joint/Erasure.ma (modified)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/utilities/binary/positive.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/extranat.ma (modified)

	Add type of maps on positive binary numbers, and use them for ...


Tue, 21 Jun 2011 00:02:37 GMT sacerdot [1014]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/FoldStuff.ma (modified)
	* src/ASM/StatusProofs.ma (added)

	The main theorem is completely broken (again).