nipkow [Tue, 31 May 2005 12:16:42 +0200] rev 16154
\nexists
nipkow [Tue, 31 May 2005 12:16:24 +0200] rev 16153
\nexists und premsise1 .. 9
wenzelm [Tue, 31 May 2005 11:53:43 +0200] rev 16152
no_tac;
wenzelm [Tue, 31 May 2005 11:53:42 +0200] rev 16151
ML Pure: name spaces have been refined;
ML Pure: cases produced by proof methods specify options, NONE means to removee bindings;
wenzelm [Tue, 31 May 2005 11:53:41 +0200] rev 16150
moved is_ident to General/symbol.ML;
wenzelm [Tue, 31 May 2005 11:53:40 +0200] rev 16149
Theory.restore_naming;
tuned fold;
wenzelm [Tue, 31 May 2005 11:53:39 +0200] rev 16148
make: T option -- actually remove undefined cases;
Logic.nth_prem;
tuned;
wenzelm [Tue, 31 May 2005 11:53:38 +0200] rev 16147
renamed cond_extern to extern;
support general naming context;
added qualified_names, no_base_names, custom_accesses, restore_naming;
removed qualified, restore_qualified;
add_cases: RuleCases.T option;
put_thms etc.: back to simple form, use naming context for extended functionality;