added option of Haskell serializer

continued

Added freshness context to FCBs.

Adapted to changes in FCBs.

Added Compile and Height examples.

Added Compile and Height examples to Nominal directory.

removed antisym_setup.ML

cleaned up

final Haskell serializer

dropped classop shallow namespace

added Haskell

added reserved words for Haskell

slight cleanup

extended section on code generator

small refinements

continued

added entries for tutorials

Proof of "bs # fK bs us vs" no longer depends on FCBs.

example of a single-step proof reconstruction

Fixed the "exception Empty" bug in elim2Fol Also added a check to suppress elimination rules that would yield too many clauses More debugging info

Added more debugging info

nclauses no longer requires its input to be in NNF

cleanup

explicit change of code width possible

code nofunc now permits theorems violating typing discipline

abandoned foldl

fold cleanup

slight cleanup

slight adaption

added normal post setup; cleaned up "execution" constants

added normal post setup

added if_delayed

started tutorial

code_constsubst -> code_axioms

Symtab.foldl replaced by Symtab.fold

Induction rule for graph of recursion combinator is now hidden to prevent name collisions with induction rule for nominal datatype.

Split up FCBs into separate formulae for each binder.

cleaning up

adapted to Stefan's new inductive package and cleaning up

Switched function package to use the new package for inductive predicates.

More robust error handling in make_nnf and forward_res

Stylistic improvements.

Restructured and repaired code dealing with case names in induction and elimination rules.

macbroy6 still has non-standard setup

moved HOL code generator setup to Code_Generator

slight cleanup

fixed print translations for bounded quantification

added explicit print translation for nat_case

added isactrlconst

Order and lattice structures no longer based on records.

add experimental macbroy6 (intel-darwin)

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;

'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