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;
wenzelm [Tue, 31 May 2005 11:53:37 +0200] rev 16146
method_cases: RuleCases.T option;
goal cases: remove previous ones;
invoke_case: ProofContext.no_base_names o ProofContext.qualified_names;
undefined rule_context: remove instead of empty one;
tuned;