added syntax interface; tuned interface;

added add_modesyntax; tuned;

added 'const_syntax';

added add_const_syntax, add_consts_authentic; tuned interface;

added syntax interface;

tuned concrete syntax -- abbreviation/const_syntax;

updated;

updated;

* Pure/library: divide_and_conquer; * Theory Real: new method ferrack;

replaced references to the robot by the mailing list page

added a much simpler proof for the iteration and recursion combinator - this also fixes a bug which prevented the nightly build from being build (sorry)

Amine Chaieb: Ferrante and Rackoff Algorithm;

Sign.certify_sort;

tuned;

removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);

avoid low-level Term.str_of_term;

abstract interfaces for type algebra; tuned;

added divide_and_conquer combinator (by Amine Chaieb); removed remains of old option type; removed obsolete eq_opt; removed obsolete string_of_bool (use Bool.toString instead); tuned;

added low-level string_of_term (back again from term.ML) -- should avoid this altogether;

more abstract interface to classes/arities;

replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);

added Ferrante and Rackoff Algorithm -- by Amine Chaieb;

fixed handling of absolute urls

added the lemmas pt_fresh_aux and pt_fresh_aux_ineq (they are used in the proof of the strong induction principle) added code to nominal_atoms to collect these lemmas in "fresh_aux" instantiated for each atom type deleted the fresh_fun_eqvt from nominal_atoms, since fresh_fun is not used anymore in the recursion combinator

reactivated translations for less/less_eq;

added add_primrec_unchecked_i;

unchecked definitions;

defs (unchecked overloaded), including former primrec; tuned;

updated;

add_defs: unchecked flag; tuned;

'defs': unchecked flag;

Theory.add_defs(_i): added unchecked flag;

added add_defs_unchecked(_i);

actually reject malformed defs; added unchecked flag; tuned;

moved defs explanation to isar-ref;

added defs (unchecked)''; more explanations on well-formednes of defs;

* Pure: overloaded definitions are now actually checked for acyclic dependencies;

tuned;

added lemma in_measure

fixed silly bug in function serializer for ML

add new finite chain theorems

improved propagate_deps; removed structs_less, which is actually unsound in conjunction with interdependent overloaded consts;

check result against certified prop, i.e. admit non-normal statements;

tuned;

avoid raw equality on type thm;

replaced Graph.fold_nodes by general Graph.fold;

added fold; removed fold_nodes; added IntGraph; tuned;

tuned Defs.merge;

allow dependencies of disjoint collections of instances; major cleanup;

use IntGraph from Pure;

Function Package: Quick-and-dirty-fixed strange "Proved a different theorem bug" due to abbreviations

Fix: Auto term must apply wf-intro rules repeatedly.

fixed codegen bug, cleanup

revert accidental text change;

introduced characters for code generator; some improved code lemmas for some list functions

added .cvsignore

added ExecutableRat.thy

removed 1::int

added preprocs for CodegenTheorems

improved code generation for wfrec

added codegen preprocessors for numerals

adaption to CodegenTheorems

added DatatypeHooks

different object logic setup for CodegenTheorems

major refinement of codegen_theorems.ML

removed superfluous eq_ord

improved chmod/chgrp handling

speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac

quoted 'termination' command;

Defs.define: const_typargs;

added raw_string_of_sort/typ/term;

simple substructure test for typargs (independent type constructors);

tuned;

string_of_option tuned

* Isar: removed obsolete 'concl is' patterns.

removed 'concl is' pattern;

removed 'concl is' patterns;

tuned;

function-package: Changed record usage to make sml/nj happy...

get rid of 'concl is';

more robust pretty_term_typ, using well-typed parse tree representation;

replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;

replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR; add_types etc.: reject qualified dummy types -- prevents users from messing up some internal conventions;

added class_error and exception CLASS_ERROR (supercedes DOMAIN); clarified of_class_derivation; tuned witness_sorts;

added syntax for _type_constraint_;

extern_early: improved handling of undeclared constants;

replaced Graph.find_paths by Graph.irreducible_paths;

of_sort: explicit cache value; simplified internal representation of instances;

axiomatization;

* Library: theory Accessible_Part has been move to main HOL.

Theory.definitions_of;

added definitions_of;

specifications_of: more detailed information; tuned;

Added small example theory for new function package.

string_of_... functions added

added the lemma pt_fresh_bij2

added something

First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.

added something

added the lemma abs_fun_eq' to the nominal theory, and also added code to nominal_atoms for generating the theorem-list alpha'

extensive reformatting and cleaning up code (no changes in functionality)

slight fix

added world map

added js

Rat.one added

fixed some flaws

fixed some flaws

added world map

pre_cnf_tac: beta-eta-normalization restricted to the current subgoal

improvments in mail obfuscator

converted to isar theory; removed unsound adm_all axiom

update to reflect changes in inverts/injects lemmas

inverts and injects generated lemmas now take the form of rewrite rules, instead of dest rules

added lemma fresh_right, which is useful in the proof of the recursion combinator

added the_theory;

extend/remove_syntax: observe inout flag for translations, too;

handle exception SYS_ERROR;

abbreviation: observe local syntax mode;

added set_syntax_mode, restore_syntax_mode;

sys_error: exception SYS_ERROR;