nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 03:12:50 +0100] rev 323

tuned

Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 02:53:23 +0100] rev 322

flagged qenv-stuff as obsolete

Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 02:49:39 +0100] rev 321

simplified get_fun so that it uses directly rty and qty, instead of qenv

Christian Urban <urbanc@in.tum.de> [Fri, 20 Nov 2009 13:03:01 +0100] rev 320

started regularize of rtrm/qtrm version; looks quite promising

Christian Urban <urbanc@in.tum.de> [Thu, 19 Nov 2009 14:17:10 +0100] rev 319

updated to new Isabelle

Christian Urban <urbanc@in.tum.de> [Wed, 18 Nov 2009 23:52:48 +0100] rev 318

fixed the storage of qconst definitions

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 13 Nov 2009 19:32:12 +0100] rev 317

Still don't know how to do the proof automatically.

Christian Urban <urbanc@in.tum.de> [Fri, 13 Nov 2009 16:44:36 +0100] rev 316

added some tracing information to all phases of lifting to the function lift_thm

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 12 Nov 2009 13:57:20 +0100] rev 315

merge of the merge?

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 12 Nov 2009 13:56:07 +0100] rev 314

merged

nominal2