2006-10-12 ago wenzelm renamed print_lthms to print_facts, do not insist on proof state;
2006-10-12 ago wenzelm print_evaluated_term: Toplevel.context_of;
2006-10-12 ago wenzelm replaced attributes_update by map_attributes;
2006-10-12 ago wenzelm Toplevel.local_theory_to_proof: proper target;
2006-10-12 ago wenzelm Toplevel.local_theory: proper target;
2006-10-12 ago urbanc To be consistent with "induct", I renamed "fixing" to "arbitrary".
2006-10-12 ago paulson Extended combinators now disabled
2006-10-12 ago paulson abstraction is now turned OFF...
2006-10-12 ago paulson Logging of theorem names to the /tmp directory now works
2006-10-12 ago wenzelm cc: avoid space after options;
2006-10-12 ago wenzelm set DYLD_LIBRARY_PATH (for Darwin);
2006-10-12 ago wenzelm added execute/system;
2006-10-12 ago wenzelm added x86-darwin;
2006-10-12 ago haftmann now allowing subdirectories in Doc/
2006-10-12 ago haftmann added makefile layer
2006-10-11 ago wenzelm * isabelle-process: option -S (secure mode) disables some critical operations;
2006-10-11 ago wenzelm increased heap size for polyml-4.9.1;
2006-10-11 ago wenzelm tuned Toplevel.begin_local_theory;
2006-10-11 ago wenzelm exit_local_theory: pass interactive flag;
2006-10-11 ago wenzelm exit: pass interactive flag;
2006-10-11 ago wenzelm added begin parser;
2006-10-11 ago wenzelm is_sid: disallow 'begin' keyword as identifier;
2006-10-11 ago wenzelm exit: pass interactive flag, toplevel result convention;
2006-10-11 ago wenzelm add_defs: declare terms;
2006-10-11 ago wenzelm 'context': demand 'begin', support local theory;
2006-10-11 ago wenzelm removed 'undo_end', recovered 'cannot_undo';
2006-10-11 ago wenzelm tuned signature;
2006-10-11 ago haftmann minor refinements in serialization
2006-10-11 ago haftmann adapted to signature change
2006-10-11 ago haftmann slight type signature changes
2006-10-11 ago haftmann cleaned up HOL bootstrap
2006-10-11 ago haftmann abandoned findrep
2006-10-11 ago haftmann added code generator setup
2006-10-11 ago haftmann added code lemma
2006-10-11 ago paulson Abstraction re-use code now checks that the abstraction function can be used in the current
2006-10-11 ago haftmann added examples for nested let
2006-10-11 ago haftmann added tex files to CVS
2006-10-11 ago wenzelm renamed body_context_node to presentation_context;
2006-10-11 ago wenzelm add_locale(_i): return actual result context;
2006-10-11 ago wenzelm class(_i): mimic Locale.add_locale(_i);
2006-10-11 ago wenzelm added type global_theory -- theory or local_theory;
2006-10-11 ago wenzelm added begin;
2006-10-11 ago wenzelm added opt_begin;
2006-10-11 ago wenzelm added raw_theory(_result);
2006-10-11 ago wenzelm Toplevel.end_proof;
2006-10-11 ago wenzelm 'end': handle local theory;
2006-10-11 ago wenzelm undo_end/kill: handle local theory;
2006-10-11 ago wenzelm Toplevel: generic_theory;
2006-10-10 ago urbanc made some proof look more like the ones in Barendregt
2006-10-10 ago paulson A way to call the ATP linkup from ML scripts
2006-10-10 ago paulson Combinators require the theory name; added settings for SPASS
2006-10-10 ago haftmann stripped pointless head
2006-10-10 ago haftmann gen_rem(s) abandoned in favour of remove / subtract
2006-10-10 ago haftmann added IsarAdvanced material
2006-10-10 ago krauss Induction rules have schematic variables again.
2006-10-10 ago haftmann initial draft
2006-10-10 ago haftmann *** empty log message ***
2006-10-10 ago haftmann initial draft
2006-10-10 ago haftmann fixed intendation
2006-10-10 ago haftmann cleanup basic HOL bootstrap