2010-02-19 |
wenzelm |
Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
|
file |
diff |
annotate
|
2009-11-08 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
2009-10-29 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
2009-10-27 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
2009-10-21 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
2009-10-21 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
2009-10-20 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
2009-10-19 |
wenzelm |
uniform use of Integer.add/mult/sum/prod;
|
file |
diff |
annotate
|
2009-10-15 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
2009-09-29 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
2009-07-30 |
wenzelm |
qualified Subgoal.FOCUS;
|
file |
diff |
annotate
|
2009-07-26 |
wenzelm |
replaced old METAHYPS by FOCUS;
|
file |
diff |
annotate
|
2009-07-20 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
2009-07-10 |
haftmann |
dropped find_index_eq
|
file |
diff |
annotate
|
2009-06-15 |
haftmann |
made SML/NJ happy
|
file |
diff |
annotate
|
2009-06-09 |
boehmes |
tuned
|
file |
diff |
annotate
|
2009-06-08 |
boehmes |
fast_lin_arith uses proper multiplication instead of unfolding to additions
|
file |
diff |
annotate
|
2009-05-11 |
haftmann |
mk_number replaces number_of
|
file |
diff |
annotate
|
2009-03-23 |
haftmann |
tuned error messages
|
file |
diff |
annotate
|
2009-03-10 |
webertj |
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
|
file |
diff |
annotate
|
2008-05-29 |
wenzelm |
added warning_count for issued reconstruction failure messages (limit 10);
|
file |
diff |
annotate
|
2008-05-18 |
wenzelm |
renamed type decompT to decomp;
|
file |
diff |
annotate
|
2008-05-07 |
berghofe |
Lookup and union operations on terms are now modulo eta conversion.
|
file |
diff |
annotate
|
2007-10-08 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
2007-09-18 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
2007-08-01 |
wenzelm |
simplified internal Config interface;
|
file |
diff |
annotate
|
2007-07-30 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
2007-07-29 |
wenzelm |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|
2007-07-04 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
2007-06-29 |
haftmann |
tuned arithmetic modules
|
file |
diff |
annotate
|
2007-06-08 |
wenzelm |
simplified type integer;
|
file |
diff |
annotate
|
2007-06-05 |
haftmann |
tuned integers
|
file |
diff |
annotate
|
2007-06-02 |
webertj |
cosmetic
|
file |
diff |
annotate
|
2007-06-01 |
webertj |
additional tracing information
|
file |
diff |
annotate
|
2007-06-01 |
webertj |
fixed handling of meta-logic propositions
|
file |
diff |
annotate
|
2007-05-21 |
haftmann |
tuned
|
file |
diff |
annotate
|
2007-05-19 |
haftmann |
dropped nonsense comment
|
file |
diff |
annotate
|
2007-05-13 |
haftmann |
tuned
|
file |
diff |
annotate
|
2007-05-06 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
2007-04-04 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
2007-04-03 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
file |
diff |
annotate
|
2006-10-31 |
haftmann |
dropped nth_update
|
file |
diff |
annotate
|
2006-08-30 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
2006-08-02 |
webertj |
type annotations fixed (IntInf.int, to make SML/NJ happy)
|
file |
diff |
annotate
|
2006-08-01 |
webertj |
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
|
file |
diff |
annotate
|
2006-07-31 |
webertj |
code reformatted
|
file |
diff |
annotate
|
2006-07-29 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
2006-07-26 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
2006-05-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2006-04-29 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2006-04-27 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
2006-03-24 |
berghofe |
Removed occurrences of makestring, which does not
|
file |
diff |
annotate
|
2006-03-22 |
webertj |
comment fixed
|
file |
diff |
annotate
|
2006-03-22 |
webertj |
comment for conjI added
|
file |
diff |
annotate
|
2006-02-15 |
wenzelm |
counter example: avoid vacuous trace;
|
file |
diff |
annotate
|
2006-01-19 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
2006-01-04 |
nipkow |
removed pointless trace msg.
|
file |
diff |
annotate
|
2005-12-02 |
haftmann |
introduced new map2, fold
|
file |
diff |
annotate
|
2005-10-28 |
haftmann |
cleaned up nth, nth_update, nth_map and nth_string functions
|
file |
diff |
annotate
|
2005-10-21 |
haftmann |
introduced functions from Pure/General/rat.ML
|
file |
diff |
annotate
|