#
# ChangeLog for src/ASM/Interpret.ma
#
# Generated by Trac 1.2
# Mar 9, 2021, 3:30:50 AM

Thu, 23 Jun 2011 00:56:20 GMT sacerdot [1037]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)

	Main theorem: comments are working again.


Thu, 16 Jun 2011 14:50:23 GMT sacerdot [985]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/common/AST.ma (modified)

	1) Major refactoring: proofs moved where they should be.
	2) New ...


Fri, 10 Jun 2011 14:20:47 GMT sacerdot [936]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)

	Ticks are now handled correctly everywhere and the main proof takes ...


Thu, 09 Jun 2011 16:07:29 GMT sacerdot [928]
	* src/ASM/Interpret.ma (modified)

	Technical splitting.


Thu, 09 Jun 2011 08:36:35 GMT mulligan [910]
	* src/ASM/Interpret.ma (modified)

	removed bug in execute_1_pseudoinstruction


Tue, 31 May 2011 09:45:21 GMT sacerdot [865]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)

	Renaming.


Mon, 30 May 2011 11:44:45 GMT sacerdot [856]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Util.ma (modified)

	1. if_then_else is now a notation for match with (to allow Russell to ...


Wed, 25 May 2011 13:57:42 GMT sacerdot [843]
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)

	Function moved from Interpret to Status.


Tue, 24 May 2011 11:26:43 GMT sacerdot [827]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)

	The preamble is now part of the PseudoStatus.


Mon, 23 May 2011 16:12:51 GMT mulligan [825]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)

	lots of refactoring, finally got something to prove


Mon, 23 May 2011 14:22:13 GMT mulligan [822]
	* src/ASM/Interpret.ma (modified)

	removed all axioms


Mon, 23 May 2011 13:23:17 GMT mulligan [821]
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)

	changes to introduce pseudostatus


Fri, 20 May 2011 16:09:00 GMT mulligan [820]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/Interpret.ma (modified)

	changes to get the semantics of pseudoassembly working


Mon, 18 Apr 2011 10:30:53 GMT mulligan [757]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/I8051.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/JointLTLLIN.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/Registers.ma (modified)

	Lots more fixing to get both front and backends using same ...


Mon, 28 Mar 2011 15:40:51 GMT mulligan [712]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Util.ma (modified)

	Changes to get things to typecheck.


Fri, 18 Mar 2011 12:47:53 GMT mulligan [698]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/I8051.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/String.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/utilities/BitVectorTrieSet.ma (modified)
	* src/utilities/StringTools.ma (modified)

	Commit with changes to files to get our files to typecheck.


Fri, 18 Mar 2011 10:34:13 GMT mulligan [690]
	* src/ASM/ASM.ma (copied)
	* src/ASM/Arithmetic.ma (copied)
	* src/ASM/BitVector.ma (copied)
	* src/ASM/BitVectorTrie.ma (copied)
	* src/ASM/Char.ma (copied)
	* src/ASM/Fetch.ma (copied)
	* src/ASM/Interpret.ma (copied)
	* src/ASM/Status.ma (copied)
	* src/ASM/String.ma (copied)
	* src/ASM/Util.ma (copied)
	* src/ASM/Vector.ma (copied)
	* src/ASM/new-matita-development (deleted)

	Moved new matita files into correct place.


Fri, 18 Mar 2011 10:31:32 GMT mulligan [688]
	* Deliverables/D4.1/Demo-March-2011 (deleted)
	* Deliverables/D4.2-4.3/LIN/LinToAsm.ma (deleted)
	* src (added)
	* src/ASM (moved)
	* src/LIN (moved)
	* src/LIN/LIN.ma (copied)

	Fixed local conflicts.  Restructured svn repository.