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;

'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;

Toplevel.end_proof;

'end': handle local theory; 'locale': begin local theory;

undo_end/kill: handle local theory; Toplevel: generic_theory;

Toplevel: generic_theory;

made some proof look more like the ones in Barendregt

A way to call the ATP linkup from ML scripts

Combinators require the theory name; added settings for SPASS

stripped pointless head

gen_rem(s) abandoned in favour of remove / subtract

added IsarAdvanced material

Induction rules have schematic variables again.

initial draft

*** empty log message ***

initial draft

fixed intendation

cleanup basic HOL bootstrap

added legacy tactic

purged some ML legacy

added eq_True eq_False True_implies_equals to extraction_expand

no breaks for Haskell

removed experimental codegen_simtype

added keeping of funcgr

generalized purge

changed order

removed quote in serialization

added code_abstype

added code_constsubst

fixed typo

added code_abstype and code_constsubst

isabelle-process: options -S, -X;

tuned;

loop: disallow exit in secure mode;

Secure.commit;

moved Context.ml_output to Output.ml_output;

Secure critical operations.

added General/secure.ML;

added option -S (secure mode);

added nbe_post for delayed_if

added delayed_if

added pre/post-processor equations

attribute "symmetric": standardized schematic variables;

sequential lemmas;

reorderd ML/lemmas (Why!?);

PureThy.note_thmss_i;

added exit; notes: simplified locale target;

added theorems(_i) -- with present_results;

def(_i): LocalDefs.add_defs; removed Drule.strip_shyps_warning;

attribute: Context.mapping; removed Drule.strip_shyps_warning;