berghofe [Thu, 03 Apr 2008 17:52:51 +0200] rev 26533
Deleted code for axiomatic introduction of datatypes. Instead, the package
now uses SkipProof.prove rather than Goal.prove to do proofs.
berghofe [Thu, 03 Apr 2008 17:50:50 +0200] rev 26532
Removed QuickAndDirty constructor from simproc_dist datatype.
berghofe [Thu, 03 Apr 2008 17:49:39 +0200] rev 26531
- use SkipProof.prove_global instead of Goal.prove_global
- added skip_mono flag to inductive definition package
berghofe [Thu, 03 Apr 2008 17:43:01 +0200] rev 26530
Added prove_global.
krauss [Thu, 03 Apr 2008 16:34:52 +0200] rev 26529
Function package no longer overwrites theorems.
Some tuning.
wenzelm [Thu, 03 Apr 2008 16:03:59 +0200] rev 26528
Why XML notation?
wenzelm [Thu, 03 Apr 2008 16:03:57 +0200] rev 26527
Symbol.STX, Symbol.DEL;
wenzelm [Thu, 03 Apr 2008 16:03:56 +0200] rev 26526
Symbol.SOH;
wenzelm [Thu, 03 Apr 2008 16:03:55 +0200] rev 26525
added detect;
removed auxiliary buffer_of_tree;
tuned;
wenzelm [Thu, 03 Apr 2008 16:03:54 +0200] rev 26524
added some ASCII control symbols;