tuned setsum rewrites

* Pure/Syntax: In schematic variable names, *any* symbol following \<^isub> or \<^isup> is now treated as part of the base name;

interpreters for lfp/gfp added

obsolete;

spassshell and testout.py are used to filter the proof part out of SPASS's output (i.e. cuts out input and search information).

tuned pretty_sg; tuned;

node_trans: revert to original transaction code (pre 1.54);

use: not a theory command!

converted back from 0..< to <.

added email

tuned trace info (depth)

simplifier trace info; Suc-intervals

some adaptions

Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML. Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and consequently removed modUnix.ML from Reconstruction.thy

tuned;

string FindTheorems.criterion;

added read_criterion/pretty_criterion; improved rule filters -- intro excludes elim rules; tuned output; tuned;

added show_dummy_patterns;

updated;

Retrieve theorems from proof context -- improved version of thms_containing by Rafal Kolanski, NICTA;

added Pure/simplifier.ML, Pure/Isar/find_theorems.ML;

moved everything related to thms_containing to find_theorems.ML; export is_known; added fact_index_of, valid_thms; gen_read': removed unused dummies option; declare_term(_syntax): canonical argument order; removed declare_terms(_syntax);

added reserved;

added ident_with;

fold ProofContext.declare_term;

added 'print_simpset'; tuned 'thms_containing'; removed 'print_intros';

added print_simpset; renamed print_thms_containing to find_theorems; removed print_intros (superceded by find_theorems intro);

added find_theorems.ML, ../simplifier.ML;

tuned terms_of_tpairs;

added string_of_thmref, selections, fact_index_of, valid_thms; moved find_matching_thms, is_matching_thm, find_intros/intros_goal/elims to Isar/find_theorems.ML; tuned

FindTheorems.print_theorems;

findI/Es/E: adapted to FindTheorems.find_XXX, results use thmref instead of string;

major tuning;

Simplifier already setup in Pure;

tuned antiquotations;

tuned thms_containing;

tuned;

moved to Pure;

moved here from Provers; removed find_rewrites (superceded by find_theorems rewrite); outer syntax moved to Pure/Isar/isar_syn.ML;

removed find_rewrites (superceded by improved thms_containing);

bug fixes for clause form transformation

converted some problems to Isar format

subst again

Skolemization of simprules and classical rules

pcpo instance for type unit

lucas - bugfix to subst in assumptions: fixed index error for conditional rules.

shortened proof of adm_disj

cleaned up and shortened some proofs

lucas - fixed subst in assumptions to count redexes from left to right.

removed update_node, which is just an instance of map_node; tuned;

tuned;

updated;

searching for combination of criteria (intro, elim, dest, name, pattern)

made para on searching more readable

new cnf function taking Skolemization theorems as an extra argument

consolidation and simplification

documented new thms_containing ('rewrites' still missing)

documented new subst

proper Id line;

updated;

var_or_skolem: always print question mark for vars stemming from skolems;

added read_variable: optional question mark on input; removed obsolete token_assoc; scan_indexname: improved treatment of \<^isub> and \<^isup>; read_var: more robust against bad input; tuned;

substantial tuning -- adapted to common conventions;

re-init ml_prompts after loop termination;

renamed show_var_qmarks to show_question_marks; renamed TermStyle.lookup_style to TermStyle.the_style;

Syntax.read_variable;

renamed show_var_qmarks to show_question_marks; string_of_vname: improved treatment of \<^isub> and \<^isup>;

renamed show_var_qmarks to show_question_marks; var_or_skolem: proper treatment of show_question_marks via Syntax.read_variable;

updated;

renamed show_var_qmarks to show_question_marks;

removed ISAMODE settings;

no longer support isa-FOO interface; removed Isamode; tuned;

no longer support isa-FOO interface;

tuned;

obsolete;

added comment

streamlined proof using new subst method

moved credit to CONTRIBUTORS;

moved credit to CONTRIBUTORS; tuned;

tuned;

export ISABELLE_HOME, do not normalize; tuned;

removed THIS_IS_ISABELLE_ADMIN;

removed rev_append; tuned presentation of datatype option: removed apsome, export the and if_none;

obsolete;

added;

proper treatment of directory links; tuned;

use Drule.vars_of_terms

Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ

searching for thms by combination of criteria (intro, elim, dest, name, term pattern)

export parser for "-"

line wrap

Eta-expanded merge function (to make SmlNJ happy).

added Proof.context to antiquotation

lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)

-(n::nat) is now regarded as atomic

Bugfix in syntax translation for record type.