add experimental at64 poly-4.9.1 test on atbroy101

generate devel snapshot even if experimental builds fail. experimental builds are those whose log files fit the pattern isatest-*e.log

added peek;

added theorem(_i);

export map_elem; added read_context_statement_i (internal locale name);

added assert;

theorem: added local_theory version;

Attrib.pretty_attrib;

added pretty_attribs (from attrib.ML);

moved pretty_attribs to attrib.ML;

locale begin/end;

updated;

Added keywords for new inductive definition package.

Adapted to changes in FixedPoint theory.

Moved old inductive package to old_inductive_package.ML

Completely rewrote inductive definition package. Now allows to define n-ary predicates directly (rather than sets of n-tuples), using generalized fixpoint theory for arbitrary complete lattices.

Old version of inductive definition package (for sets).

Moved old inductive package to old_inductive_package.ML

Adapted to new inductive definition package.

Adapted to changes in FixedPoint theory.

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;