nipkow [Sun, 09 Apr 2006 14:31:37 +0200] rev 19377
*** empty log message ***
nipkow [Sun, 09 Apr 2006 14:20:23 +0200] rev 19376
Removed old set interval syntax.
wenzelm [Sat, 08 Apr 2006 22:51:35 +0200] rev 19375
pretty_term: late externing of consts (support authentic syntax);
wenzelm [Sat, 08 Apr 2006 22:51:33 +0200] rev 19374
pretty: late externing of consts (support authentic syntax);
wenzelm [Sat, 08 Apr 2006 22:51:31 +0200] rev 19373
removed fix_mixfix;
added const_mixfix, mixfix_const;
wenzelm [Sat, 08 Apr 2006 22:51:30 +0200] rev 19372
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm [Sat, 08 Apr 2006 22:51:28 +0200] rev 19371
add_abbrevs(_i): support print mode;
pretty_term': expand abbreviations only for well-typed terms;
added expand_abbrevs;
tuned;
wenzelm [Sat, 08 Apr 2006 22:51:26 +0200] rev 19370
abbrevs: support print mode;
wenzelm [Sat, 08 Apr 2006 22:51:25 +0200] rev 19369
simplified handling of authentic syntax (cf. early externing in consts.ML);
simplified extern_term;
wenzelm [Sat, 08 Apr 2006 22:51:23 +0200] rev 19368
'abbreviation': optional print mode;
wenzelm [Sat, 08 Apr 2006 22:51:22 +0200] rev 19367
tuned;
wenzelm [Sat, 08 Apr 2006 22:51:20 +0200] rev 19366
pretty_term': early vs. late externing (support authentic syntax);
add_abbrevs(_i): support print mode and authentic syntax;
wenzelm [Sat, 08 Apr 2006 22:51:19 +0200] rev 19365
print_theory: print abbreviations nicely;
wenzelm [Sat, 08 Apr 2006 22:51:17 +0200] rev 19364
added intern/extern/extern_early;
added expand_abbrevs flag;
strip_abss: demand ocurrences of bounds in body;
const decl: added flag for early externing (disabled for authentic syntax);
abbrevs: support print mode;
major cleanup;
wenzelm [Sat, 08 Apr 2006 22:51:06 +0200] rev 19363
refined 'abbreviation';
haftmann [Sat, 08 Apr 2006 22:12:02 +0200] rev 19362
made symlink relative
haftmann [Sat, 08 Apr 2006 22:10:58 +0200] rev 19361
made symlink relative
kleing [Sat, 08 Apr 2006 15:24:21 +0200] rev 19360
converted Müller to Mueller to make smlnj 110.58 work
berghofe [Fri, 07 Apr 2006 17:27:53 +0200] rev 19359
Fixed bug that caused proof of induction rule to fail
for inductive sets with trivial introduction rules
such as "x : S ==> x : S".
kleing [Fri, 07 Apr 2006 12:48:10 +0200] rev 19358
remame ASeries to Arithmetic_Series
berghofe [Fri, 07 Apr 2006 11:17:44 +0200] rev 19357
Added alternative version of thms_of_proof that does not recursively
descend into proofs of (named) theorems.
mengj [Fri, 07 Apr 2006 05:14:54 +0200] rev 19356
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
mengj [Fri, 07 Apr 2006 05:14:06 +0200] rev 19355
filter now accepts axioms as thm, instead of term.
mengj [Fri, 07 Apr 2006 05:12:51 +0200] rev 19354
tptp_write_file accepts axioms as thm.
mengj [Fri, 07 Apr 2006 05:12:23 +0200] rev 19353
added another function for CNF.
mengj [Fri, 07 Apr 2006 05:12:00 +0200] rev 19352
lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.
kleing [Fri, 07 Apr 2006 03:20:34 +0200] rev 19351
renamed ASeries to Arithmetic_Series, removed the ^M
urbanc [Thu, 06 Apr 2006 17:29:40 +0200] rev 19350
modified the perm_compose rule such that it
is applied as simplification rule (as simproc)
in the restricted case where the first
permutation is a swapping coming from a supports
problem
also deleted the perm_compose' rule from the set
of rules that are automatically tried
haftmann [Thu, 06 Apr 2006 16:13:17 +0200] rev 19349
cleanup in typedef/datatype package
haftmann [Thu, 06 Apr 2006 16:12:57 +0200] rev 19348
added explicit serialization for int equality
haftmann [Thu, 06 Apr 2006 16:11:30 +0200] rev 19347
adapted for definitional code generation
haftmann [Thu, 06 Apr 2006 16:10:46 +0200] rev 19346
cleanup in datatype package
haftmann [Thu, 06 Apr 2006 16:10:22 +0200] rev 19345
small type annotation fix
haftmann [Thu, 06 Apr 2006 16:09:54 +0200] rev 19344
added hook for codegen_theorems.ML
haftmann [Thu, 06 Apr 2006 16:09:37 +0200] rev 19343
adaptions to change in typedef_package.ML
haftmann [Thu, 06 Apr 2006 16:09:20 +0200] rev 19342
added functions for definitional code generation
haftmann [Thu, 06 Apr 2006 16:08:25 +0200] rev 19341
added definitional code generator module: codegen_theorems.ML
haftmann [Thu, 06 Apr 2006 16:08:22 +0200] rev 19340
minor changes
haftmann [Thu, 06 Apr 2006 16:07:44 +0200] rev 19339
exported specification names
haftmann [Wed, 05 Apr 2006 17:38:32 +0200] rev 19338
minor extensions
paulson [Wed, 05 Apr 2006 12:47:38 +0200] rev 19337
pool of constants; definition expansion; current best settings
paulson [Fri, 31 Mar 2006 10:53:33 +0200] rev 19336
removed some illegal characters: they were crashing SML/NJ
paulson [Fri, 31 Mar 2006 10:52:20 +0200] rev 19335
Removal of unused code
paulson [Tue, 28 Mar 2006 16:48:18 +0200] rev 19334
Simplified version of Jia's filter. Now all constants are pooled, rather than
relevance being compared against separate clauses. Rejects are no longer noted,
and units cannot be added at the end.
schirmer [Tue, 28 Mar 2006 12:11:33 +0200] rev 19333
renamed map_val to map_ran
schirmer [Tue, 28 Mar 2006 12:05:45 +0200] rev 19332
added map_val, superseding map_at and substitute
----------------------------------------------------------------------
haftmann [Tue, 28 Mar 2006 10:13:51 +0200] rev 19331
some internal cleanup
paulson [Mon, 27 Mar 2006 18:10:02 +0200] rev 19330
removed illegal character codes
urbanc [Sun, 26 Mar 2006 03:22:42 +0200] rev 19329
simplified the proof at_fin_set_supp
nipkow [Sat, 25 Mar 2006 18:16:07 +0100] rev 19328
changed abbreviation for "infinite" back to translation because
something didn't work during (output).
huffman [Fri, 24 Mar 2006 19:30:01 +0100] rev 19327
lazy patterns in lambda abstractions
urbanc [Fri, 24 Mar 2006 15:59:16 +0100] rev 19326
changed the it_prm proof to work for recursion
urbanc [Fri, 24 Mar 2006 15:15:08 +0100] rev 19325
tuned some proofs
berghofe [Fri, 24 Mar 2006 11:54:07 +0100] rev 19324
Removed occurrences of makestring, which does not
exist in SML/NJ.
nipkow [Thu, 23 Mar 2006 20:03:53 +0100] rev 19323
Converted translations to abbbreviations.
Removed a few odd functions from Map and AssocList.
Moved chg_map from Map to Bali/Basis.
berghofe [Thu, 23 Mar 2006 18:14:06 +0100] rev 19322
Replaced iteration combinator by recursion combinator.
paulson [Thu, 23 Mar 2006 10:05:03 +0100] rev 19321
detection of definitions of relevant constants
mengj [Thu, 23 Mar 2006 06:18:38 +0100] rev 19320
Only display atpset theorems if Output.show_debug_msgs is true.
urbanc [Wed, 22 Mar 2006 18:09:35 +0100] rev 19319
added the first two simple proofs of the recursion
combinator
webertj [Wed, 22 Mar 2006 14:06:29 +0100] rev 19318
comment fixed