paulson [Wed, 22 Mar 2006 12:33:44 +0100] rev 19317
Introduction of "whitelist": theorems forced past the relevance filter
paulson [Wed, 22 Mar 2006 12:32:44 +0100] rev 19316
Slight simplification of proofs
paulson [Wed, 22 Mar 2006 12:30:29 +0100] rev 19315
Removal of obsolete strategies. Initial support for locales: Frees and Consts
treated similarly.
webertj [Wed, 22 Mar 2006 11:54:54 +0100] rev 19314
comment for conjI added
nipkow [Wed, 22 Mar 2006 11:14:58 +0100] rev 19313
translations -> abbreviations (a cool feature)
wenzelm [Tue, 21 Mar 2006 15:38:53 +0100] rev 19312
fixed example;
wenzelm [Tue, 21 Mar 2006 12:18:22 +0100] rev 19311
mark_boundT: produce well-typed term;
wenzelm [Tue, 21 Mar 2006 12:18:21 +0100] rev 19310
subtract (op =);
pretty_proof: no abbrevs;
wenzelm [Tue, 21 Mar 2006 12:18:20 +0100] rev 19309
avoid polymorphic equality;
tuned;
wenzelm [Tue, 21 Mar 2006 12:18:19 +0100] rev 19308
avoid polymorphic equality;
subtract (op =);
wenzelm [Tue, 21 Mar 2006 12:18:18 +0100] rev 19307
moved gen_eq_set to library.ML;
wenzelm [Tue, 21 Mar 2006 12:18:17 +0100] rev 19306
added ~$$ (negative literal);
combinators: avoid code duplication;
tuned extend_lexicon;
wenzelm [Tue, 21 Mar 2006 12:18:15 +0100] rev 19305
avoid polymorphic equality;
wenzelm [Tue, 21 Mar 2006 12:18:13 +0100] rev 19304
remove (op =);
tuned;
wenzelm [Tue, 21 Mar 2006 12:18:11 +0100] rev 19303
gen_eq_set, remove (op =);
wenzelm [Tue, 21 Mar 2006 12:18:10 +0100] rev 19302
abbreviation upto, length;
wenzelm [Tue, 21 Mar 2006 12:18:09 +0100] rev 19301
added subtract;
tuned;
wenzelm [Tue, 21 Mar 2006 12:18:07 +0100] rev 19300
subtract (op =);
wenzelm [Tue, 21 Mar 2006 12:18:06 +0100] rev 19299
remove (op =);
paulson [Tue, 21 Mar 2006 12:17:38 +0100] rev 19298
Now SML/NJ-friendly (IntInf)
paulson [Tue, 21 Mar 2006 12:16:43 +0100] rev 19297
Removal of unnecessary simprules: simproc cancel_numerals now works without
add_Suc, while the reason for the horrible isolateSuc is not known.
wenzelm [Mon, 20 Mar 2006 21:29:04 +0100] rev 19296
interpret: Proof.assert_forward_or_chain;
paulson [Mon, 20 Mar 2006 17:38:22 +0100] rev 19295
subsetI is often necessary
paulson [Mon, 20 Mar 2006 17:37:11 +0100] rev 19294
Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer
need to be outermost.
ballarin [Mon, 20 Mar 2006 17:15:35 +0100] rev 19293
Tuned signature of Locale.add_locale(_i).
wenzelm [Sat, 18 Mar 2006 20:10:51 +0100] rev 19292
simplified mg_domain (use Sign.classes/arities_of);
removed unused lift_local_theory_yield;
wenzelm [Sat, 18 Mar 2006 20:10:50 +0100] rev 19291
made $$ and "this" monomorphic (string);
wenzelm [Sat, 18 Mar 2006 20:10:49 +0100] rev 19290
tuned;
wenzelm [Sat, 18 Mar 2006 20:10:48 +0100] rev 19289
export arities_of instead of classes_arities_of;
wenzelm [Sat, 18 Mar 2006 18:33:49 +0100] rev 19288
updated;
wenzelm [Sat, 18 Mar 2006 18:33:40 +0100] rev 19287
renamed const less to lt;
haftmann [Sat, 18 Mar 2006 09:58:49 +0100] rev 19286
renamed constant less in lattice
nipkow [Fri, 17 Mar 2006 22:33:06 +0100] rev 19285
fixed problem with proof reconstruction by adding add_Suc to arith-simpset.
schirmer [Fri, 17 Mar 2006 17:38:38 +0100] rev 19284
added parser locale_expr_unless
haftmann [Fri, 17 Mar 2006 16:17:38 +0100] rev 19283
fixed clsvar bug
ballarin [Fri, 17 Mar 2006 15:22:40 +0100] rev 19282
add_locale(_i) returns internal locale name.
haftmann [Fri, 17 Mar 2006 14:20:24 +0100] rev 19281
added example for operational classes and code generator
haftmann [Fri, 17 Mar 2006 14:19:24 +0100] rev 19280
slight improvement in serializer, stub for code generator theorems added
ballarin [Fri, 17 Mar 2006 10:04:27 +0100] rev 19279
Renamed setsum_mult to setsum_right_distrib.
ballarin [Fri, 17 Mar 2006 09:57:25 +0100] rev 19278
Internal restructuring: local parameters.
haftmann [Fri, 17 Mar 2006 09:34:23 +0100] rev 19277
renamed op < <= to Orderings.less(_eq)
ballarin [Thu, 16 Mar 2006 20:19:25 +0100] rev 19276
New interface function parameters_of_expr.
berghofe [Wed, 15 Mar 2006 17:59:33 +0100] rev 19275
add_inst_arity_i renamed to prove_arity.
wenzelm [Wed, 15 Mar 2006 16:18:12 +0100] rev 19274
rename_frees: treat trivial names;
monomorphic: tuned invented names;
wenzelm [Tue, 14 Mar 2006 22:07:33 +0100] rev 19273
added singleton;
wenzelm [Tue, 14 Mar 2006 22:06:43 +0100] rev 19272
updated;
wenzelm [Tue, 14 Mar 2006 22:06:42 +0100] rev 19271
turned string_of_mixfix into pretty_mixfix;
wenzelm [Tue, 14 Mar 2006 22:06:40 +0100] rev 19270
added monomorphic;
export hidden_polymorphism;
wenzelm [Tue, 14 Mar 2006 22:06:39 +0100] rev 19269
added 'print_statement' command;
wenzelm [Tue, 14 Mar 2006 22:06:37 +0100] rev 19268
added print_stmts;
wenzelm [Tue, 14 Mar 2006 22:06:36 +0100] rev 19267
added pretty_statement;
wenzelm [Tue, 14 Mar 2006 22:06:35 +0100] rev 19266
added command, keyword;
added chunks2;
wenzelm [Tue, 14 Mar 2006 22:06:33 +0100] rev 19265
Output.add_mode: keyword component;
wenzelm [Tue, 14 Mar 2006 22:06:31 +0100] rev 19264
string_of_mixfix;
wenzelm [Tue, 14 Mar 2006 22:06:29 +0100] rev 19263
print_statement;
wenzelm [Tue, 14 Mar 2006 16:29:39 +0100] rev 19262
added remove_trrules(_i);
tuned;
wenzelm [Tue, 14 Mar 2006 16:29:38 +0100] rev 19261
added is_elim (from Provers/classical.ML);
wenzelm [Tue, 14 Mar 2006 16:29:37 +0100] rev 19260
added 'no_translations';
wenzelm [Tue, 14 Mar 2006 16:29:36 +0100] rev 19259
added pretty_stmt;
tuned;
wenzelm [Tue, 14 Mar 2006 16:29:35 +0100] rev 19258
declared_const: check for type constraint only, i.e. admit abbreviations as well;
added del_trrules(_i);
wenzelm [Tue, 14 Mar 2006 16:29:34 +0100] rev 19257
ObjectLogic.is_elim;
wenzelm [Tue, 14 Mar 2006 16:29:32 +0100] rev 19256
tuned constdecl;
added 'no_translations';
wenzelm [Tue, 14 Mar 2006 16:29:31 +0100] rev 19255
updated;
wenzelm [Tue, 14 Mar 2006 16:29:29 +0100] rev 19254
Pure: no_translations;
haftmann [Tue, 14 Mar 2006 14:25:09 +0100] rev 19253
refined representation of instance dictionaries
schirmer [Mon, 13 Mar 2006 10:41:04 +0100] rev 19252
entry for Library/AssocList
berghofe [Mon, 13 Mar 2006 00:09:23 +0100] rev 19251
First version of function for defining graph of iteration combinator.
wenzelm [Sat, 11 Mar 2006 21:23:10 +0100] rev 19250
got rid of type Sign.sg;
wenzelm [Sat, 11 Mar 2006 17:30:35 +0100] rev 19249
renamed plus to add;
wenzelm [Sat, 11 Mar 2006 17:24:37 +0100] rev 19248
renamed const minus to subtract;
wenzelm [Sat, 11 Mar 2006 16:56:09 +0100] rev 19247
simplified AxClass interfaces;
wenzelm [Sat, 11 Mar 2006 16:53:28 +0100] rev 19246
added axclass_instance_XXX (from axclass.ML);
Sign.read/cert_arity;
wenzelm [Sat, 11 Mar 2006 16:53:27 +0100] rev 19245
*** empty log message ***
wenzelm [Sat, 11 Mar 2006 16:53:23 +0100] rev 19244
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm [Sat, 11 Mar 2006 16:53:20 +0100] rev 19243
moved read_class, read/cert_classrel/arity to sign.ML;
axclass: moved outer syntax to isar_syn.ML;
instance: moved to Tools/class_package.ML;
simplified interfaces;
tuned;
wenzelm [Sat, 11 Mar 2006 16:53:14 +0100] rev 19242
use axclass.ML earlier (in Isar/ROOT.ML);
wenzelm [Sat, 11 Mar 2006 16:53:10 +0100] rev 19241
nbe: no_document;
wenzelm [Fri, 10 Mar 2006 19:49:58 +0100] rev 19240
tuned;
paulson [Fri, 10 Mar 2006 17:57:09 +0100] rev 19239
exporting reapAll and killChild
webertj [Fri, 10 Mar 2006 17:53:53 +0100] rev 19238
text delimiter fixed
webertj [Fri, 10 Mar 2006 17:24:16 +0100] rev 19237
comment delimiter fixed
webertj [Fri, 10 Mar 2006 16:31:50 +0100] rev 19236
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
haftmann [Fri, 10 Mar 2006 16:21:49 +0100] rev 19235
fix for document preparation
schirmer [Fri, 10 Mar 2006 16:05:34 +0100] rev 19234
Added Library/AssocList.thy
haftmann [Fri, 10 Mar 2006 15:33:48 +0100] rev 19233
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
paulson [Fri, 10 Mar 2006 12:28:38 +0100] rev 19232
Changed some warnings to debug messages
paulson [Fri, 10 Mar 2006 12:27:36 +0100] rev 19231
Frequency analysis of constants (with types).
Ability to restrict the number of accepted clauses.
mengj [Fri, 10 Mar 2006 04:03:48 +0100] rev 19230
Shortened the exception messages from assume.
mengj [Fri, 10 Mar 2006 04:02:53 +0100] rev 19229
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
huffman [Fri, 10 Mar 2006 00:53:28 +0100] rev 19228
added many simple lemmas
mengj [Thu, 09 Mar 2006 06:05:01 +0100] rev 19227
Added more functions to the signature and tidied up some functions.
wenzelm [Wed, 08 Mar 2006 21:40:46 +0100] rev 19226
tuned;
urbanc [Wed, 08 Mar 2006 18:52:43 +0100] rev 19225
tuned some proofs
wenzelm [Wed, 08 Mar 2006 18:37:31 +0100] rev 19224
select_goals: split original conjunctions;
wenzelm [Wed, 08 Mar 2006 18:37:30 +0100] rev 19223
method: goal restriction defaults to [1];
wenzelm [Wed, 08 Mar 2006 18:37:28 +0100] rev 19222
infer_derivs: avoid allocating empty MinProof;
wenzelm [Wed, 08 Mar 2006 18:37:27 +0100] rev 19221
tuned;
wenzelm [Wed, 08 Mar 2006 18:37:25 +0100] rev 19220
Isar/method: goal restriction;
wenzelm [Wed, 08 Mar 2006 18:37:24 +0100] rev 19219
constdecl: always allow 'where';
urbanc [Wed, 08 Mar 2006 18:00:00 +0100] rev 19218
deleted some proofs "on comment"
urbanc [Wed, 08 Mar 2006 17:55:51 +0100] rev 19217
tuned some proofs
urbanc [Wed, 08 Mar 2006 17:54:55 +0100] rev 19216
tuned some of the proofs about fresh_fun
haftmann [Wed, 08 Mar 2006 17:23:46 +0100] rev 19215
first running version of type classes
haftmann [Wed, 08 Mar 2006 17:03:19 +0100] rev 19214
first running version of type classes
haftmann [Wed, 08 Mar 2006 16:29:07 +0100] rev 19213
first running version of type classes
paulson [Wed, 08 Mar 2006 10:19:57 +0100] rev 19212
Frequency strategy. Revised indentation, etc.
nipkow [Wed, 08 Mar 2006 10:06:31 +0100] rev 19211
*** empty log message ***
obua [Tue, 07 Mar 2006 18:02:11 +0100] rev 19210
added ROOT.ML
paulson [Tue, 07 Mar 2006 16:50:33 +0100] rev 19209
Indentation
paulson [Tue, 07 Mar 2006 16:49:48 +0100] rev 19208
Tidying and restructuring.
paulson [Tue, 07 Mar 2006 16:49:12 +0100] rev 19207
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
paulson [Tue, 07 Mar 2006 16:47:51 +0100] rev 19206
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
Removal of the unused err_list.
paulson [Tue, 07 Mar 2006 16:46:54 +0100] rev 19205
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson [Tue, 07 Mar 2006 16:45:04 +0100] rev 19204
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
obua [Tue, 07 Mar 2006 16:03:31 +0100] rev 19203
Added HOL-ZF to Isabelle.
haftmann [Tue, 07 Mar 2006 14:09:48 +0100] rev 19202
substantial improvement in codegen iml
mengj [Tue, 07 Mar 2006 04:06:02 +0100] rev 19201
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
The hash table (for removing duplicate) now stores clauses as Term.term with names.
mengj [Tue, 07 Mar 2006 04:04:21 +0100] rev 19200
relevance_filter takes input axioms as Term.term.
mengj [Tue, 07 Mar 2006 04:01:25 +0100] rev 19199
Proof reconstruction now only takes names of theorems as input.
mengj [Tue, 07 Mar 2006 03:59:48 +0100] rev 19198
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj [Tue, 07 Mar 2006 03:58:50 +0100] rev 19197
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
mengj [Tue, 07 Mar 2006 03:56:59 +0100] rev 19196
Added functions to retrieve local and global atpset rules.
cnf thms to Term.term format.
mengj [Tue, 07 Mar 2006 03:54:11 +0100] rev 19195
Moved the settings for ATP time limit to res_atp.ML
mengj [Tue, 07 Mar 2006 03:51:40 +0100] rev 19194
Merged res_atp_setup.ML into res_atp.ML.
HOL translation is integrated with background Isabelle-ATP linkup.
Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.
mengj [Tue, 07 Mar 2006 03:49:26 +0100] rev 19193
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
mengj [Tue, 07 Mar 2006 03:48:02 +0100] rev 19192
Merged res_atp_setup.ML into res_atp.ML.
wenzelm [Sun, 05 Mar 2006 23:56:57 +0100] rev 19191
SELECT_GOAL: fixed trivial case;
webertj [Sun, 05 Mar 2006 18:49:13 +0100] rev 19190
fixed a typo in a comment
wenzelm [Sat, 04 Mar 2006 21:39:08 +0100] rev 19189
tuned;
wenzelm [Sat, 04 Mar 2006 21:10:12 +0100] rev 19188
method: SelectGoals;
wenzelm [Sat, 04 Mar 2006 21:10:11 +0100] rev 19187
method: syntax for SelectGoals;
wenzelm [Sat, 04 Mar 2006 21:10:10 +0100] rev 19186
text: added SelectGoals;
wenzelm [Sat, 04 Mar 2006 21:10:09 +0100] rev 19185
tuned conj_curry;
wenzelm [Sat, 04 Mar 2006 21:10:08 +0100] rev 19184
added extract, retrofit;
wenzelm [Sat, 04 Mar 2006 21:10:07 +0100] rev 19183
added mk_conjunction;
tuned conj_curry;
wenzelm [Sat, 04 Mar 2006 21:10:06 +0100] rev 19182
method: restriction to first n sub-goals;
nipkow [Fri, 03 Mar 2006 19:43:46 +0100] rev 19181
minor changes
nipkow [Fri, 03 Mar 2006 19:30:30 +0100] rev 19180
more examples
nipkow [Fri, 03 Mar 2006 19:30:20 +0100] rev 19179
changed and retracted change of location of code lemmas.
nipkow [Fri, 03 Mar 2006 16:25:30 +0100] rev 19178
ignore repeated vars on lhs, cleanup
haftmann [Fri, 03 Mar 2006 08:52:39 +0100] rev 19177
improvements for nbe
paulson [Thu, 02 Mar 2006 18:51:11 +0100] rev 19176
reformatting
paulson [Thu, 02 Mar 2006 18:50:43 +0100] rev 19175
subset_refl now included using the atp attribute
paulson [Thu, 02 Mar 2006 18:49:13 +0100] rev 19174
moved the "use" directive
urbanc [Thu, 02 Mar 2006 16:01:06 +0100] rev 19173
fixed the bugs itroduced by the previous commit
urbanc [Thu, 02 Mar 2006 15:43:22 +0100] rev 19172
made some small changes to generate nicer latex-output
urbanc [Thu, 02 Mar 2006 15:05:09 +0100] rev 19171
split the files
- Iteration.thy contains the big proof of the iteration combinator
- Recursion.thy derives from Iteration the recursion combinator
- lam_substs.thy contains the examples (size, substitution and parallel substitution)
mengj [Thu, 02 Mar 2006 00:57:34 +0100] rev 19170
Added in a signature.
urbanc [Wed, 01 Mar 2006 18:26:20 +0100] rev 19169
fixed a problem where a permutation is not analysed
when the term is of the form
(pi o f) x1...xn
This was the case because the head of this term is the
constant "nominal.perm". Now an applicability predicate
decides the right behaviour of the simproc
urbanc [Wed, 01 Mar 2006 18:24:31 +0100] rev 19168
streamlined the proof
haftmann [Wed, 01 Mar 2006 13:47:42 +0100] rev 19167
refined representation of codegen intermediate language
urbanc [Wed, 01 Mar 2006 10:37:00 +0100] rev 19166
some small tunings
urbanc [Wed, 01 Mar 2006 10:28:39 +0100] rev 19165
added fresh_fun_eqvt theorem to the theorem collection
urbanc [Wed, 01 Mar 2006 10:27:48 +0100] rev 19164
added initialisation-code for finite_guess
urbanc [Wed, 01 Mar 2006 10:27:01 +0100] rev 19163
made some small tunings in the decision-procedure
(in the order how the "small" tactics are called)
mengj [Wed, 01 Mar 2006 06:08:12 +0100] rev 19162
Added setup for "atpset" (a rule set for ATPs).
mengj [Wed, 01 Mar 2006 06:06:16 +0100] rev 19161
Added file Tools/res_atpset.ML.
mengj [Wed, 01 Mar 2006 06:05:25 +0100] rev 19160
Merged HOL and FOL clauses and combined some functions.
mengj [Wed, 01 Mar 2006 05:56:53 +0100] rev 19159
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
urbanc [Wed, 01 Mar 2006 00:04:52 +0100] rev 19158
some minor tuning on the proofs
urbanc [Tue, 28 Feb 2006 12:28:22 +0100] rev 19157
initial commit (especially 2nd half needs to be cleaned up)
paulson [Tue, 28 Feb 2006 11:10:51 +0100] rev 19156
removal of theory blacklist
paulson [Tue, 28 Feb 2006 11:09:50 +0100] rev 19155
new order for arity clauses
paulson [Tue, 28 Feb 2006 11:09:29 +0100] rev 19154
fixed but in freeze_spec
paulson [Tue, 28 Feb 2006 11:07:54 +0100] rev 19153
splitting up METAHYPS into smaller functions
paulson [Tue, 28 Feb 2006 11:07:13 +0100] rev 19152
typos
urbanc [Mon, 27 Feb 2006 17:37:37 +0100] rev 19151
added a finite_guess tactic, which solves
automatically finite-support goals
haftmann [Mon, 27 Feb 2006 15:51:37 +0100] rev 19150
class package and codegen refinements
haftmann [Mon, 27 Feb 2006 15:49:56 +0100] rev 19149
added nbe
nipkow [Mon, 27 Feb 2006 14:34:03 +0100] rev 19148
added temp. nbe test
nipkow [Mon, 27 Feb 2006 14:03:31 +0100] rev 19147
added nbe, updated neb_*
nipkow [Mon, 27 Feb 2006 14:03:15 +0100] rev 19146
added nbe
ballarin [Mon, 27 Feb 2006 12:20:21 +0100] rev 19145
Typo.
urbanc [Mon, 27 Feb 2006 12:14:36 +0100] rev 19144
added support for arbitrary atoms in the simproc
wenzelm [Sun, 26 Feb 2006 23:01:50 +0100] rev 19143
put_thms: do_index;
wenzelm [Sun, 26 Feb 2006 23:01:48 +0100] rev 19142
rewrite_goals_rule_aux: actually use prems if present;
wenzelm [Sun, 26 Feb 2006 23:01:47 +0100] rev 19141
add_local: do_index;
urbanc [Sun, 26 Feb 2006 22:25:17 +0100] rev 19140
replaced the lemma at_two by at_different;
this lemma now proves
EX b. a != b
urbanc [Sun, 26 Feb 2006 22:24:05 +0100] rev 19139
improved the decision-procedure for permutations;
now uses a simproc
FIXME:
the simproc still needs to be adapted for arbitrary
atom types
haftmann [Sat, 25 Feb 2006 15:19:47 +0100] rev 19138
improved codegen bootstrap
haftmann [Sat, 25 Feb 2006 15:19:19 +0100] rev 19137
change in codegen syntax
haftmann [Sat, 25 Feb 2006 15:19:00 +0100] rev 19136
some refinements
haftmann [Sat, 25 Feb 2006 15:11:35 +0100] rev 19135
added more detailed data to consts
berghofe [Fri, 24 Feb 2006 17:48:17 +0100] rev 19134
Reverted to old interface of AxClass.add_inst_arity(_i)
berghofe [Fri, 24 Feb 2006 09:00:21 +0100] rev 19133
Adapted to Florian's recent changes to the AxClass package.
urbanc [Thu, 23 Feb 2006 20:56:31 +0100] rev 19132
added lemmas
at_two: EX a b in an atom type such that a !=b
at_ds10
and a "test"-lemma at_prm_eq_compose (can probably be removed)
wenzelm [Thu, 23 Feb 2006 13:37:46 +0100] rev 19131
make SML/NJ happy;
mengj [Thu, 23 Feb 2006 13:00:18 +0100] rev 19130
Default type level is T_FULL now.
mengj [Thu, 23 Feb 2006 12:59:01 +0100] rev 19129
eprover removes tmp files too.
mengj [Thu, 23 Feb 2006 12:57:39 +0100] rev 19128
vampire/eprover methods can now be applied repeatedly until they fail.
wenzelm [Wed, 22 Feb 2006 22:18:42 +0100] rev 19127
removed obsolete meta_conjunction_tr';
wenzelm [Wed, 22 Feb 2006 22:18:41 +0100] rev 19126
rew: handle conjunctionI/D1/D2;
wenzelm [Wed, 22 Feb 2006 22:18:39 +0100] rev 19125
simplified Pure conjunction, based on actual const;
wenzelm [Wed, 22 Feb 2006 22:18:38 +0100] rev 19124
removed rename_indexes_wrt;
added rename_indexes2;
simplified Pure conjunction, based on actual const;
wenzelm [Wed, 22 Feb 2006 22:18:36 +0100] rev 19123
renamed class_axms to class_intros;
wenzelm [Wed, 22 Feb 2006 22:18:33 +0100] rev 19122
tuned proofs;
wenzelm [Wed, 22 Feb 2006 22:18:32 +0100] rev 19121
simplified Pure conjunction;
wenzelm [Wed, 22 Feb 2006 22:18:31 +0100] rev 19120
not_equal: replaced syntax translation by abbreviation;
simplified Pure conjunction;
haftmann [Wed, 22 Feb 2006 10:18:17 +0100] rev 19119
abandoned merge_alists' in favour of generic AList.merge
nipkow [Tue, 21 Feb 2006 16:37:54 +0100] rev 19118
added Tools/nbe, fixes
nipkow [Tue, 21 Feb 2006 16:37:33 +0100] rev 19117
added Tools/nbe
nipkow [Tue, 21 Feb 2006 16:18:50 +0100] rev 19116
New normalization-by-evaluation package
wenzelm [Tue, 21 Feb 2006 15:06:50 +0100] rev 19115
distinct (op =);
removed spurious PolyML.print;
kleing [Mon, 20 Feb 2006 21:51:50 +0100] rev 19114
fixed
paulson [Mon, 20 Feb 2006 16:23:38 +0100] rev 19113
Inclusion of subset_refl in ATP calls
paulson [Mon, 20 Feb 2006 16:22:52 +0100] rev 19112
Fix variable-naming bug (?) by removing a needless recursive call
haftmann [Mon, 20 Feb 2006 11:38:06 +0100] rev 19111
slight code generator serialization improvements
haftmann [Mon, 20 Feb 2006 11:37:18 +0100] rev 19110
moved intro_classes from AxClass to ClassPackage
kleing [Sun, 19 Feb 2006 22:40:18 +0100] rev 19109
fixed document
kleing [Sun, 19 Feb 2006 22:12:30 +0100] rev 19108
* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
#3 in http://www.cs.ru.nl/~freek/100/
urbanc [Sun, 19 Feb 2006 17:18:39 +0100] rev 19107
added a few lemmas to do with permutation-equivalence for the
recursion combinator
kleing [Sun, 19 Feb 2006 13:21:32 +0100] rev 19106
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
* added Complex/ex/ASeries_Complex (instantiation of the above for reals)
* added Complex/ex/HarmonicSeries (should really be in something like Complex/Library)
(these are contributions by Benjamin Porter, numbers 68 and 34 of
http://www.cs.ru.nl/~freek/100/)
huffman [Sun, 19 Feb 2006 02:11:27 +0100] rev 19105
use minimal imports
huffman [Sun, 19 Feb 2006 01:40:13 +0100] rev 19104
use qualified name for return
wenzelm [Sat, 18 Feb 2006 18:08:23 +0100] rev 19103
dest_def: tuned error msg;
wenzelm [Fri, 17 Feb 2006 20:03:21 +0100] rev 19102
const constraints: provide TFrees instead of TVars,
actually delete constraint (allows Consts.merge caused by ProofContext.transfer after qed);
wenzelm [Fri, 17 Feb 2006 20:03:19 +0100] rev 19101
checkpoint/copy_node: reset body context;
wenzelm [Fri, 17 Feb 2006 20:03:17 +0100] rev 19100
global_qeds: transfer body context;
wenzelm [Fri, 17 Feb 2006 20:03:14 +0100] rev 19099
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
wenzelm [Fri, 17 Feb 2006 20:03:10 +0100] rev 19098
constrain: assert const declaration, optional type (i.e. may delete constraints);
wenzelm [Fri, 17 Feb 2006 17:00:33 +0100] rev 19097
removed Import/lazy_scan.ML;
paulson [Fri, 17 Feb 2006 15:43:46 +0100] rev 19096
hyperlinks in the PDF work now
obua [Fri, 17 Feb 2006 15:03:26 +0100] rev 19095
replaced Symbol.explode by explode
haftmann [Fri, 17 Feb 2006 08:42:41 +0100] rev 19094
updated mailing list archive link
obua [Fri, 17 Feb 2006 03:30:50 +0100] rev 19093
use monomorphic sequences / scanners
huffman [Fri, 17 Feb 2006 01:46:38 +0100] rev 19092
make maybe into a real type constructor; remove monad syntax
obua [Thu, 16 Feb 2006 23:40:32 +0100] rev 19091
use VectorScannerSeq instead of ListScannerSeq in xml.ML
obua [Thu, 16 Feb 2006 23:31:32 +0100] rev 19090
removed lazy_scan
obua [Thu, 16 Feb 2006 23:30:47 +0100] rev 19089
improved scanning
wenzelm [Thu, 16 Feb 2006 21:15:38 +0100] rev 19088
tuned;
wenzelm [Thu, 16 Feb 2006 21:12:03 +0100] rev 19087
Abstract Natural Numbers with polymorphic recursion.
wenzelm [Thu, 16 Feb 2006 21:12:00 +0100] rev 19086
new-style definitions/abbreviations;
wenzelm [Thu, 16 Feb 2006 21:11:58 +0100] rev 19085
added ex/Abstract_NAT.thy;
wenzelm [Thu, 16 Feb 2006 19:39:02 +0100] rev 19084
tuned;
wenzelm [Thu, 16 Feb 2006 19:10:47 +0100] rev 19083
tuned;
haftmann [Thu, 16 Feb 2006 18:59:39 +0100] rev 19082
removed silly stuff
wenzelm [Thu, 16 Feb 2006 18:39:48 +0100] rev 19081
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm [Thu, 16 Feb 2006 18:26:04 +0100] rev 19080
added abbreviation(_i);
wenzelm [Thu, 16 Feb 2006 18:26:03 +0100] rev 19079
added put_thms_internal: local_naming, no fact index;
tuned;
wenzelm [Thu, 16 Feb 2006 18:26:02 +0100] rev 19078
added put_thms_internal;
tuned;