wenzelm [Thu, 17 Jan 2002 21:00:38 +0100] rev 12797
eta_contract with sharing (by berghofe);
rewrite_term: proper handling of Abs cong;
wenzelm [Thu, 17 Jan 2002 20:59:46 +0100] rev 12796
is_norm_hhf moved to drule.ML;
wenzelm [Thu, 17 Jan 2002 20:59:31 +0100] rev 12795
added timeap_msg;
nipkow [Thu, 17 Jan 2002 19:37:57 +0100] rev 12794
new style theory
nipkow [Thu, 17 Jan 2002 19:37:42 +0100] rev 12793
Lex dependencies modified
nipkow [Thu, 17 Jan 2002 19:32:22 +0100] rev 12792
Added code generation to Scanner.thy
Renamed Union -> Or, union -> or
kleing [Thu, 17 Jan 2002 15:06:36 +0100] rev 12791
registered directly executable version with the code generator
nipkow [Thu, 17 Jan 2002 12:58:31 +0100] rev 12790
*** empty log message ***
paulson [Thu, 17 Jan 2002 12:45:52 +0100] rev 12789
new definitions from Sidi Ehmety
paulson [Thu, 17 Jan 2002 12:45:36 +0100] rev 12788
made proofs more robust
paulson [Thu, 17 Jan 2002 10:35:59 +0100] rev 12787
mistakenly deleted this theory
kleing [Thu, 17 Jan 2002 09:01:10 +0100] rev 12786
fixed
wenzelm [Wed, 16 Jan 2002 23:19:34 +0100] rev 12785
GPLed;
wenzelm [Wed, 16 Jan 2002 23:18:20 +0100] rev 12784
added rewrite_term;
tuned;
GPLed;