adapted to new serializer syntax

constructing proof

dropped constructiv `->

new serialization syntax; experimental extensions

refined

refined algorithm

simplified preprocessor framework

cleanup

*** empty log message ***

fixed type signature of Type.varify

dropped junk

disabled some code generation (an intermeidate solution)

adapted to new serializer syntax

added Equals_conv

cleaned up

adaptions to changes in preprocessor

dropped nth_update

Purely cosmetic

new file for defining functions in the lambda-calculus

Added "recdef_wf" and "simp" attribute to "wf_measures"

Removed debugging output

removed free "x" from termination goal...

Added "measures" combinator for lexicographic combinations of multiple measures.

Conversion to clause form now tolerates Boolean variables without looping. Attribute "clausify" moved to res_axioms; rest of reconstruction.ML deleted

adapted to Stefan's new inductive package

Fixed bug in the handling of congruence rules

(added entry)

switched merge_alists'' to AList.merge'' whenever appropriate

new single-step proofs

meson method MUST NOT use all safe rules, only basic ones for the logical connectives.

Improved tracing

fixed two bugs

bugfixes

added example with split

cleanup in ML setup code

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

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;

removed obsolete note_thmss(_i); simplified add_thmss; tuned;

added exit;

simplified derived_def;

removed theorems, smart_theorems etc. (cf. Specification.theorems);

lemmas/theorems/declare: Specification.theorems;

added kind attributes;

Drule.lhs/rhs_of;

added dest_equals_lhs; replaced clhs/crhs_of by lhs/rhs_of; local_standard: flexflex_unique; removed strip_shyps_warning;

attribute: Context.mapping; Proof.theorem_i;

replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;