isabelle update -u control_cartouches;

adapted ZF,FOL,CCL,LCF to modified splitter

more explicit context;

proper context for Object_Logic operations;

clarified Drule.gen_all: observe context more carefully;

tuned signature -- prefer qualified names;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

proper context for assume_tac (atac remains as fall-back without context);

proper context for match_tac etc.;

eliminated aliases;

more qualified names;

tuned signature;
clarified context;

simplifier uses proper Proof.context instead of historic type simpset;

avoid stepping outside of context -- plain zero_var_indexes should be sufficient;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

tuned signature;

simplified/unified Simplifier.mk_solver;

proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;

modernized Clasimp setup;

simplified Data signature;

misc tuning;

modernized Quantifier1 simproc setup;

clarified simpset setup;
discontinued unused old-style FOL_css;

proper identifiers for consts and types;

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

more antiquotations

removed some old comments;

proper context for rule_by_tactic;

proper context for mksimps etc. -- via simpset of the running Simplifier;

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

explicitly qualify Drule.standard;

replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;

renamed functor SplitterFun to Splitter, require explicit theory;

more @{theory} antiquotations;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

more antiquotations;

removed obsolete CVS Ids;

Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;

back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;

ML_Antiquote.value;

purely functional setup of claset/simpset/clasimpset;

eliminated out-of-scope proofs (cf. theory IFOL and FOL);
proper antiquotations;

removed obsolete induct/simp tactic;

added @{clasimpset};

converted legacy ML scripts;

tuned proofs;

setup: theory -> theory;

removed obsolete Provers/make_elim.ML;

unfold_tac: static evaluation of simpset;

Simplifier.theory_context;

change_claset/simpset;
Simplifier.inherit_context instead of Simplifier.inherit_bounds;

introduced new-style AList operations

simprocs: Simplifier.inherit_bounds;

Simplifier already setup in Pure;

Move towards standard functions.

Deleted Library.option type.

sane interface for simprocs;

better simplification of trivial existential equalities

new simprules and classical rules

new theorem

renamed forall_elim_vars_safe to gen_all;

replace gen_all by forall_elim_vars_safe;

mods due to changed 1-point simprocs (quantifier1).

proper use of bind_thm(s);

moved rulify to ObjectLogic;

eliminated atomize rules;

streamlined addIffs/delIffs, added warnings

generalization of 1 point rules for ALL

FOL_basic_ss: simprocs moved to FOL_ss;

rulify setup;

iff declarations moved to clasimp.ML;

cong setup now part of Simplifier;

AddIffs now available for FOL, ZF

added cong atts;

clasimp: include Splitter;

Mod because of new solver interface.

proper bootstrap of IFOL/FOL theories and packages;

Theory.sign_of;

congruence rules finally use == instead of = and <->

simplified CLASIMP_DATA
renamed mk_meta_eq to mk_eq
introduced new mk_meta_eq,
simplified addcongs and delcongs, introducing mk_meta_cong

Pruning of parameters and True assumptions

minor adaption for SML/NJ

the splitter is now defined as a functor
moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML
moved split_thm_info to Provers/splitter.ML
definined atomize via general mk_atomize
removed superfluous rot_eq_tac from simplifier.ML
HOL/simpdata.ML: renamed mk_meta_eq to meta_eq,
re-renamed mk_meta_eq_simp to mk_meta_eq
added Eps_eq to simpset

made SML/NJ happy;

functorized Clasimp module;

HACKED declaration of addsplits

extended addsplits and delsplits to handle also split rules for assumptions
extended const_of_split_thm, renamed it to split_thm_info

no open Simplifier;

Splitters via named loopers.

factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML
explicitly introducing combined type clasimpset

changed wrapper mechanism of classical reasoner

New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort

Instantiated the one-point-rule quantifier simpprocs for FOL

New file fologic.ML holds abstract syntax operations

Also, miniscoping provided for intuitionistic logic

addsplits now in FOL, ZF too

renamed split_prem_tac to split_asm_tac

added split_prem_tac

changed libraray function find to find_index_eq, currying it

adapted to new implicit simpset;

New simprules imp_disj1,2 and some comments

fixed dots;

Moved functions from file "thy_data.ML".

standard congs;

Removal of the tactical STATE

renamed addss to addSss, unsafe_addss to addss, extended auto_tac

Added P&P&Q <-> P&Q and P|P|Q <-> P|Q

Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors

added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
safe_asm_more_full_simp_tac
new addss (old version retained as unsafe_addss),
new auto_tac (old version retained as unsafe_auto_tac),
clasimpset with modification functions

Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
with Basis Library structure Int

Implicit simpsets and clasets for FOL and ZF

Added the de Morgan laws (incl quantifier versions) to basic simpset

Addition of one-point quantifier rewrite rules

Removal of (EX x. P) <-> P and (ALL x. P) <-> P
from ex_simps and all_simps. as they are already in quant_simps.

Introduction of miniscoping for FOL

Added a lot of basic laws, from HOL/simpdata

Added split_inside_tac.

expanded tabs

Imported meta_eq_to_obj_eq from HOL for use with 'split'.

Defined addss to perform simplification in a claset.
Precedence of addcongs is now 4 (to match that of other simplifier infixes)

Enforced partial evaluation of mk_case_split_tac.

conj_commute,disj_commute: new

added qed_goal for meta_iffD

added blank line

atomize: borrowed HOL version, which checks for both Trueprop
and == as main connective (avoids using wildcard)

Modified mk_meta_eq to leave meta-equlities on unchanged.
Thus you may now add ==-thms to simpsets.

FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
simplifier can rewrite premises, it can generate the premise False."

FOL/simpdata: tidied
FOL/simpdata/not_rews: moved the law "~(P|Q) <-> ~P & ~Q" from distrib_rews
FOL/simpdata/cla_rews: added the law "~(P&Q) <-> ~P | ~Q"

updated solver of FOL_ss. see change of HOL/simpdata.ML

Added gen_all to simpdata.ML.

defined local addcongs

Initial revision