Legacy ML bindings now refer to old inductive definition package.

Added new package for inductive definitions, moved old package to old_inductive_package.ML

Generalized gfp and lfp to arbitrary complete lattices.

Repaired strip_assums_hyp (now also works for goals not in hhf normal form).

improved framework

refined

fixed bug

tuned

added codegen2 example

added the missing freshness-lemmas for nat, int, char and string and also the lemma for permutation acting on if's

lifted claset setup from ML to Isar level

explicit nonfix for union and inter

renamed enter_forward_proof to enter_proof_body; renamed exit_local_theory to end_local_theory; added local_theory_to_proof; tuned;

added peek;

interpretation_in_locale: standalone goal setup; moved theorem statements to bottom;

tuned;

renamed print_lthms to print_facts, do not insist on proof state; renamed Toplevel.enter_forward_proof to Toplevel.enter_proof_body;

print_evaluated_term: Toplevel.context_of;

replaced attributes_update by map_attributes;

Toplevel.local_theory_to_proof: proper target;

Toplevel.local_theory: proper target; removed dead code;

To be consistent with "induct", I renamed "fixing" to "arbitrary". However I am not very fond of "arbitrary" - e.g. it clashes with "arbitrary" of HOL. Both Gentzen (at least in the Szabo translation) and Velleman (in How to prove it: a structured approach) use "arbitrary". Still, I wonder whether "generalising" is a good compromise?

Extended combinators now disabled

abstraction is now turned OFF...

Logging of theorem names to the /tmp directory now works

cc: avoid space after options;

set DYLD_LIBRARY_PATH (for Darwin);

added execute/system;

added x86-darwin;

now allowing subdirectories in Doc/

added makefile layer

* isabelle-process: option -S (secure mode) disables some critical operations;

increased heap size for polyml-4.9.1;

tuned Toplevel.begin_local_theory;

exit_local_theory: pass interactive flag; begin_local_theory: generic init;

exit: pass interactive flag; moved exit to local_theory.ML; tuned pretty;

added begin parser;

is_sid: disallow 'begin' keyword as identifier;

exit: pass interactive flag, toplevel result convention;

add_defs: declare terms;

'context': demand 'begin', support local theory; removed 'undo_end', recovered 'cannot_undo'; tuned Toplevel.begin_local_theory;

removed 'undo_end', recovered 'cannot_undo';

tuned signature;

minor refinements in serialization

adapted to signature change

slight type signature changes

cleaned up HOL bootstrap

abandoned findrep

added code generator setup

added code lemma

Abstraction re-use code now checks that the abstraction function can be used in the current theory.

added examples for nested let

added tex files to CVS

renamed body_context_node to presentation_context;

add_locale(_i): return actual result context; cert_facts: allow qualified names;

class(_i): mimic Locale.add_locale(_i); 'class': begin_local_theory;

added type global_theory -- theory or local_theory; added begin/exit_local_theory; removed theory_context; renamed body_context_node to presentation_context; removed copy (checkpoint twice instead -- avoids unrelated theories);

added begin;

added opt_begin;

added raw_theory(_result); tuned;