nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 16:52:32 +0100] rev 1154

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 16:51:30 +0100] rev 1153

Fixed the definition of less and finished the missing proof.

Christian Urban <urbanc@in.tum.de> [Mon, 15 Feb 2010 16:50:11 +0100] rev 1152

further tuning

Christian Urban <urbanc@in.tum.de> [Mon, 15 Feb 2010 16:37:48 +0100] rev 1151

small tuning

Christian Urban <urbanc@in.tum.de> [Mon, 15 Feb 2010 16:28:07 +0100] rev 1150

tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 14:58:03 +0100] rev 1149

der_bname -> derived_bname

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 14:51:17 +0100] rev 1148

Names of files.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 14:28:03 +0100] rev 1147

Finished introducing the binding.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 13:40:03 +0100] rev 1146

Synchronize the commands.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 12:23:02 +0100] rev 1145

Passing the binding to quotient_def

nominal2