unused;

clarified signature -- some operations to support fully explicit proof terms;

proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);

tuned signature;

clarified signature;
tuned;

tuned signature;

clarified export of sort algebra: avoid logical operations in Isabelle/Scala;

clarified standardization of variables, with proper treatment of local variables;
tuned signature;
tuned;

eliminated ASCII syntax from Pure bootstrap;
tuned comments;

tuned;

defs are closed, which leads to proper auto_bind_facts;
misc tuning;

avoid vacuous quantification, as usual for shared variable scope;

support for structure statements in 'assume', 'presume';

tuned whitespace;

eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;

local fixes may depend on goal params;

more qualified names;

more qualified names;

more qualified names;

clarified defer/prefer: more specific errors;

renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;

renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;

discontinued old-style Term.list_all_free in favour of plain Logic.all;

added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
tuned;

tuned signature;

tuned signature: Name.invent and Name.invent_names;

outer_constraints with original variable names, to ensure that argsP is consistent with args

just one version of Thm.unconstrainT, which affects all variables;
temporary workaround for Nbe.lift_triv_classes_conv;

added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);

Logic.mk_of_sort convenience;

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

eliminated redundant bindings;

modernized Balanced_Tree;

tuned incr_tvar_same;
export tuned version of incr_indexes_same;

export incr_tvar_same;
tuned;

use structure Same;
tuned;

removed obsolete/unused legacy_varify;

tuned comment;

removed obsolete/unused legacy_unvarify;

tuned varify/unvarify: use Term_Subst.map_XXX combinators;

renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;

substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);

moved basic algebra of long names from structure NameSpace to Long_Name;

renamed NameSpace.base to NameSpace.base_name;
renamed NameSpace.map_base to NameSpace.map_base_name;
eliminated alias Sign.base_name = NameSpace.base_name;

qualified Term.rename_wrt_term;

Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;

tuned comments;

added all, is_all;
improved dest_all;
added implies (from term.ML);

eliminated theory ProtoPure;

Removed Logic.auto_rename.

replaced literal 'a by Name.aT;

moved support for primitive defs to primitive_defs.ML;

simplified has_meta_prems;

balanced conjunctions;

removed unused is_atomic;

added is_atomic;
removed unused is_all;

removed unused mk_cond_defpair;

simplified Logic.count_prems;

added type_map;

Repaired strip_assums_hyp (now also works for goals not
in hhf normal form).

removed is_equals, is_implies;
tuned;

added name_classrel/arities/arity;

renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);

replaced Term.variant(list) by Name.variant(_list);
Name.invent_list;

(un)varify: tuned exceptions;

renamed Type.(un)varifyT to Logic.(un)varifyT;
made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;

support embedded terms;

added dest_conjunction_list;
close_form: canonical order of variables;

added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
tuned;

Term.itselfT;

simplified Pure conjunction, based on actual const;

dest_def: tuned error msg;

dest_def: actually return beta-eta contracted equation;

renamed gen_duplicates to duplicates;

added generic dest_def (mostly from theory.ML);
added abs_def (from Isar/local_defs.ML);
added const_of_class/class_of_const (from sign.ML);
added combound, rlist_abs (from unify.ML);

added dest_all;

added mk_conjunction_list2;

mk_conjunction: proper treatment of bounds;
added dest_conjunction(s);

tuned;

tuned;

renamed Goal constant to prop, more general protect/unprotect interfaces;
replaced lift_fns by lift_abs, lift_all;

optimization to incr_indexes?

incr_tvar (from term.ML), incr_indexes: avoid garbage;

tuned;

occs no longer infix (structure not open);

added nth_prem;

First version of global registration command.

thin_tac now works on P==>Q

fixed thin_tac with higher-level assumptions by removing the old code to
handle the iterated introduction of parameters

Removed extraneous rev in function goal_params (the list of parameters
is already reversed by rename_wrt_term).

Exported function goal_params.

Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML

Removed obsolete functions dealing with flex-flex constraints.

Symbol.bump_string;

is_norm_hhf moved to drule.ML;

added mk_conjunction_list;

added mk_conjunction;

added is_norm_hhf;

has_meta_prems: include "==";

fixed strip_assums and assum_pairs, restoring them (essentially) to their
1989 versions. They had been "optimized" for flattened parameters, but
failed when given an initial, non-flattened proof state. A manifestation
of the bug is

Goal "of the bug isf. EX B. Q(f,B) ==> (of the bug isy. P(f,y))";
be exE 1;

fixed has_meta_prems: strip_assums_hyp;

added has_meta_prems;

Logic.goal_const;

Goals may now contain assumptions, which are not returned.
This is controlled by an argument `atomic' to the goal commands.

added mk_cond_defpair, mk_defpair;

adapted to baroque chars;

Reorganized simplifier. May now reorient rules.
Moved loop tests from logic to thm.

Tried to reorganize rewriter a little. More to be done.

Improved loop-test for rewrite rules a little.
Should be done properly!

term order stuff moved to term.ML;

tuned term order;
added indexname_ord, typ_ord, typs_ord, term_ord, terms_ord;

Fixed the definition of `termord': is now antisymmetric.

logic: loops -> rewrite_rule_ok
added rewrite_rule_extra_vars

thm: Rewrite rules must not introduce new type vars on rhs.
This lead to an incompleteness, is now banned, and the code
has been simplified.

Corrected alphabetical order of entries in signature.

Added "op" before "occs" to make sml/nj happy

The simplifier has been improved a little: equations s=t which used to be
rejected because of looping are now treated as (s=t) == True. The latter
translation must be done outside of Thm because it involves the object-logic
specific True. Therefore the simple loop test has been moved from Thm to
Logic.

Removal of freeze_vars and thaw_vars (quite unused...)

added term order;

Replaced map...~~ by ListPair.map

Restored warning comment

Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

inserted tabs again

removed tabs

added is_equals: term -> bool;

Pure/type/unvarifyT: moved there from logic.ML

/unvarifyT, unvarify: moved to Pure/logic.ML

changed comment only;

added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
restored functor sig constraint :LOGIC;

commented out sig constraint of functor (for debugging purposes);

logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
So it no longer checks t properly -- but it never checked u anyway, and all
existing calls are derived from certified terms...

Initial revision