| Tue, 14 Mar 2006 22:06:37 +0100 |
wenzelm |
added print_stmts;
|
changeset |
files
|
| Tue, 14 Mar 2006 22:06:36 +0100 |
wenzelm |
added pretty_statement;
|
changeset |
files
|
| Tue, 14 Mar 2006 22:06:35 +0100 |
wenzelm |
added command, keyword;
|
changeset |
files
|
| Tue, 14 Mar 2006 22:06:33 +0100 |
wenzelm |
Output.add_mode: keyword component;
|
changeset |
files
|
| Tue, 14 Mar 2006 22:06:31 +0100 |
wenzelm |
string_of_mixfix;
|
changeset |
files
|
| Tue, 14 Mar 2006 22:06:29 +0100 |
wenzelm |
print_statement;
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:39 +0100 |
wenzelm |
added remove_trrules(_i);
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:38 +0100 |
wenzelm |
added is_elim (from Provers/classical.ML);
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:37 +0100 |
wenzelm |
added 'no_translations';
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:36 +0100 |
wenzelm |
added pretty_stmt;
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:35 +0100 |
wenzelm |
declared_const: check for type constraint only, i.e. admit abbreviations as well;
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:34 +0100 |
wenzelm |
ObjectLogic.is_elim;
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:32 +0100 |
wenzelm |
tuned constdecl;
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:31 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 14 Mar 2006 16:29:29 +0100 |
wenzelm |
Pure: no_translations;
|
changeset |
files
|
| Tue, 14 Mar 2006 14:25:09 +0100 |
haftmann |
refined representation of instance dictionaries
|
changeset |
files
|
| Mon, 13 Mar 2006 10:41:04 +0100 |
schirmer |
entry for Library/AssocList
|
changeset |
files
|
| Mon, 13 Mar 2006 00:09:23 +0100 |
berghofe |
First version of function for defining graph of iteration combinator.
|
changeset |
files
|
| Sat, 11 Mar 2006 21:23:10 +0100 |
wenzelm |
got rid of type Sign.sg;
|
changeset |
files
|
| Sat, 11 Mar 2006 17:30:35 +0100 |
wenzelm |
renamed plus to add;
|
changeset |
files
|
| Sat, 11 Mar 2006 17:24:37 +0100 |
wenzelm |
renamed const minus to subtract;
|
changeset |
files
|
| Sat, 11 Mar 2006 16:56:09 +0100 |
wenzelm |
simplified AxClass interfaces;
|
changeset |
files
|
| Sat, 11 Mar 2006 16:53:28 +0100 |
wenzelm |
added axclass_instance_XXX (from axclass.ML);
|
changeset |
files
|
| Sat, 11 Mar 2006 16:53:27 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Sat, 11 Mar 2006 16:53:23 +0100 |
wenzelm |
added read_class, read/cert_classrel/arity (from axclass.ML);
|
changeset |
files
|
| Sat, 11 Mar 2006 16:53:20 +0100 |
wenzelm |
moved read_class, read/cert_classrel/arity to sign.ML;
|
changeset |
files
|
| Sat, 11 Mar 2006 16:53:14 +0100 |
wenzelm |
use axclass.ML earlier (in Isar/ROOT.ML);
|
changeset |
files
|
| Sat, 11 Mar 2006 16:53:10 +0100 |
wenzelm |
nbe: no_document;
|
changeset |
files
|
| Fri, 10 Mar 2006 19:49:58 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 10 Mar 2006 17:57:09 +0100 |
paulson |
exporting reapAll and killChild
|
changeset |
files
|
| Fri, 10 Mar 2006 17:53:53 +0100 |
webertj |
text delimiter fixed
|
changeset |
files
|
| Fri, 10 Mar 2006 17:24:16 +0100 |
webertj |
comment delimiter fixed
|
changeset |
files
|
| Fri, 10 Mar 2006 16:31:50 +0100 |
webertj |
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
|
changeset |
files
|
| Fri, 10 Mar 2006 16:21:49 +0100 |
haftmann |
fix for document preparation
|
changeset |
files
|
| Fri, 10 Mar 2006 16:05:34 +0100 |
schirmer |
Added Library/AssocList.thy
|
changeset |
files
|
| Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
changeset |
files
|
| Fri, 10 Mar 2006 12:28:38 +0100 |
paulson |
Changed some warnings to debug messages
|
changeset |
files
|
| Fri, 10 Mar 2006 12:27:36 +0100 |
paulson |
Frequency analysis of constants (with types).
|
changeset |
files
|
| Fri, 10 Mar 2006 04:03:48 +0100 |
mengj |
Shortened the exception messages from assume.
|
changeset |
files
|
| Fri, 10 Mar 2006 04:02:53 +0100 |
mengj |
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
|
changeset |
files
|
| Fri, 10 Mar 2006 00:53:28 +0100 |
huffman |
added many simple lemmas
|
changeset |
files
|
| Thu, 09 Mar 2006 06:05:01 +0100 |
mengj |
Added more functions to the signature and tidied up some functions.
|
changeset |
files
|
| Wed, 08 Mar 2006 21:40:46 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 08 Mar 2006 18:52:43 +0100 |
urbanc |
tuned some proofs
|
changeset |
files
|
| Wed, 08 Mar 2006 18:37:31 +0100 |
wenzelm |
select_goals: split original conjunctions;
|
changeset |
files
|
| Wed, 08 Mar 2006 18:37:30 +0100 |
wenzelm |
method: goal restriction defaults to [1];
|
changeset |
files
|
| Wed, 08 Mar 2006 18:37:28 +0100 |
wenzelm |
infer_derivs: avoid allocating empty MinProof;
|
changeset |
files
|
| Wed, 08 Mar 2006 18:37:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 08 Mar 2006 18:37:25 +0100 |
wenzelm |
Isar/method: goal restriction;
|
changeset |
files
|
| Wed, 08 Mar 2006 18:37:24 +0100 |
wenzelm |
constdecl: always allow 'where';
|
changeset |
files
|
| Wed, 08 Mar 2006 18:00:00 +0100 |
urbanc |
deleted some proofs "on comment"
|
changeset |
files
|
| Wed, 08 Mar 2006 17:55:51 +0100 |
urbanc |
tuned some proofs
|
changeset |
files
|
| Wed, 08 Mar 2006 17:54:55 +0100 |
urbanc |
tuned some of the proofs about fresh_fun
|
changeset |
files
|
| Wed, 08 Mar 2006 17:23:46 +0100 |
haftmann |
first running version of type classes
|
changeset |
files
|
| Wed, 08 Mar 2006 17:03:19 +0100 |
haftmann |
first running version of type classes
|
changeset |
files
|
| Wed, 08 Mar 2006 16:29:07 +0100 |
haftmann |
first running version of type classes
|
changeset |
files
|
| Wed, 08 Mar 2006 10:19:57 +0100 |
paulson |
Frequency strategy. Revised indentation, etc.
|
changeset |
files
|
| Wed, 08 Mar 2006 10:06:31 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 07 Mar 2006 18:02:11 +0100 |
obua |
added ROOT.ML
|
changeset |
files
|
| Tue, 07 Mar 2006 16:50:33 +0100 |
paulson |
Indentation
|
changeset |
files
|
| Tue, 07 Mar 2006 16:49:48 +0100 |
paulson |
Tidying and restructuring.
|
changeset |
files
|
| Tue, 07 Mar 2006 16:49:12 +0100 |
paulson |
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
|
changeset |
files
|
| Tue, 07 Mar 2006 16:47:51 +0100 |
paulson |
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
|
changeset |
files
|
| Tue, 07 Mar 2006 16:46:54 +0100 |
paulson |
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
|
changeset |
files
|
| Tue, 07 Mar 2006 16:45:04 +0100 |
paulson |
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
|
changeset |
files
|
| Tue, 07 Mar 2006 16:03:31 +0100 |
obua |
Added HOL-ZF to Isabelle.
|
changeset |
files
|
| Tue, 07 Mar 2006 14:09:48 +0100 |
haftmann |
substantial improvement in codegen iml
|
changeset |
files
|
| Tue, 07 Mar 2006 04:06:02 +0100 |
mengj |
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
|
changeset |
files
|
| Tue, 07 Mar 2006 04:04:21 +0100 |
mengj |
relevance_filter takes input axioms as Term.term.
|
changeset |
files
|
| Tue, 07 Mar 2006 04:01:25 +0100 |
mengj |
Proof reconstruction now only takes names of theorems as input.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:59:48 +0100 |
mengj |
Added tptp_write_file to write all necessary ATP input clauses to one file.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:58:50 +0100 |
mengj |
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:56:59 +0100 |
mengj |
Added functions to retrieve local and global atpset rules.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:54:11 +0100 |
mengj |
Moved the settings for ATP time limit to res_atp.ML
|
changeset |
files
|
| Tue, 07 Mar 2006 03:51:40 +0100 |
mengj |
Merged res_atp_setup.ML into res_atp.ML.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:49:26 +0100 |
mengj |
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:48:02 +0100 |
mengj |
Merged res_atp_setup.ML into res_atp.ML.
|
changeset |
files
|
| Sun, 05 Mar 2006 23:56:57 +0100 |
wenzelm |
SELECT_GOAL: fixed trivial case;
|
changeset |
files
|
| Sun, 05 Mar 2006 18:49:13 +0100 |
webertj |
fixed a typo in a comment
|
changeset |
files
|
| Sat, 04 Mar 2006 21:39:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:12 +0100 |
wenzelm |
method: SelectGoals;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:11 +0100 |
wenzelm |
method: syntax for SelectGoals;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:10 +0100 |
wenzelm |
text: added SelectGoals;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:09 +0100 |
wenzelm |
tuned conj_curry;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:08 +0100 |
wenzelm |
added extract, retrofit;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:07 +0100 |
wenzelm |
added mk_conjunction;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:06 +0100 |
wenzelm |
method: restriction to first n sub-goals;
|
changeset |
files
|
| Fri, 03 Mar 2006 19:43:46 +0100 |
nipkow |
minor changes
|
changeset |
files
|
| Fri, 03 Mar 2006 19:30:30 +0100 |
nipkow |
more examples
|
changeset |
files
|
| Fri, 03 Mar 2006 19:30:20 +0100 |
nipkow |
changed and retracted change of location of code lemmas.
|
changeset |
files
|
| Fri, 03 Mar 2006 16:25:30 +0100 |
nipkow |
ignore repeated vars on lhs, cleanup
|
changeset |
files
|
| Fri, 03 Mar 2006 08:52:39 +0100 |
haftmann |
improvements for nbe
|
changeset |
files
|
| Thu, 02 Mar 2006 18:51:11 +0100 |
paulson |
reformatting
|
changeset |
files
|
| Thu, 02 Mar 2006 18:50:43 +0100 |
paulson |
subset_refl now included using the atp attribute
|
changeset |
files
|
| Thu, 02 Mar 2006 18:49:13 +0100 |
paulson |
moved the "use" directive
|
changeset |
files
|
| Thu, 02 Mar 2006 16:01:06 +0100 |
urbanc |
fixed the bugs itroduced by the previous commit
|
changeset |
files
|
| Thu, 02 Mar 2006 15:43:22 +0100 |
urbanc |
made some small changes to generate nicer latex-output
|
changeset |
files
|
| Thu, 02 Mar 2006 15:05:09 +0100 |
urbanc |
split the files
|
changeset |
files
|
| Thu, 02 Mar 2006 00:57:34 +0100 |
mengj |
Added in a signature.
|
changeset |
files
|
| Wed, 01 Mar 2006 18:26:20 +0100 |
urbanc |
fixed a problem where a permutation is not analysed
|
changeset |
files
|
| Wed, 01 Mar 2006 18:24:31 +0100 |
urbanc |
streamlined the proof
|
changeset |
files
|
| Wed, 01 Mar 2006 13:47:42 +0100 |
haftmann |
refined representation of codegen intermediate language
|
changeset |
files
|
| Wed, 01 Mar 2006 10:37:00 +0100 |
urbanc |
some small tunings
|
changeset |
files
|
| Wed, 01 Mar 2006 10:28:39 +0100 |
urbanc |
added fresh_fun_eqvt theorem to the theorem collection
|
changeset |
files
|
| Wed, 01 Mar 2006 10:27:48 +0100 |
urbanc |
added initialisation-code for finite_guess
|
changeset |
files
|
| Wed, 01 Mar 2006 10:27:01 +0100 |
urbanc |
made some small tunings in the decision-procedure
|
changeset |
files
|
| Wed, 01 Mar 2006 06:08:12 +0100 |
mengj |
Added setup for "atpset" (a rule set for ATPs).
|
changeset |
files
|
| Wed, 01 Mar 2006 06:06:16 +0100 |
mengj |
Added file Tools/res_atpset.ML.
|
changeset |
files
|
| Wed, 01 Mar 2006 06:05:25 +0100 |
mengj |
Merged HOL and FOL clauses and combined some functions.
|
changeset |
files
|
| Wed, 01 Mar 2006 05:56:53 +0100 |
mengj |
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
|
changeset |
files
|
| Wed, 01 Mar 2006 00:04:52 +0100 |
urbanc |
some minor tuning on the proofs
|
changeset |
files
|
| Tue, 28 Feb 2006 12:28:22 +0100 |
urbanc |
initial commit (especially 2nd half needs to be cleaned up)
|
changeset |
files
|
| Tue, 28 Feb 2006 11:10:51 +0100 |
paulson |
removal of theory blacklist
|
changeset |
files
|
| Tue, 28 Feb 2006 11:09:50 +0100 |
paulson |
new order for arity clauses
|
changeset |
files
|
| Tue, 28 Feb 2006 11:09:29 +0100 |
paulson |
fixed but in freeze_spec
|
changeset |
files
|
| Tue, 28 Feb 2006 11:07:54 +0100 |
paulson |
splitting up METAHYPS into smaller functions
|
changeset |
files
|
| Tue, 28 Feb 2006 11:07:13 +0100 |
paulson |
typos
|
changeset |
files
|
| Mon, 27 Feb 2006 17:37:37 +0100 |
urbanc |
added a finite_guess tactic, which solves
|
changeset |
files
|
| Mon, 27 Feb 2006 15:51:37 +0100 |
haftmann |
class package and codegen refinements
|
changeset |
files
|
| Mon, 27 Feb 2006 15:49:56 +0100 |
haftmann |
added nbe
|
changeset |
files
|
| Mon, 27 Feb 2006 14:34:03 +0100 |
nipkow |
added temp. nbe test
|
changeset |
files
|
| Mon, 27 Feb 2006 14:03:31 +0100 |
nipkow |
added nbe, updated neb_*
|
changeset |
files
|
| Mon, 27 Feb 2006 14:03:15 +0100 |
nipkow |
added nbe
|
changeset |
files
|
| Mon, 27 Feb 2006 12:20:21 +0100 |
ballarin |
Typo.
|
changeset |
files
|
| Mon, 27 Feb 2006 12:14:36 +0100 |
urbanc |
added support for arbitrary atoms in the simproc
|
changeset |
files
|
| Sun, 26 Feb 2006 23:01:50 +0100 |
wenzelm |
put_thms: do_index;
|
changeset |
files
|
| Sun, 26 Feb 2006 23:01:48 +0100 |
wenzelm |
rewrite_goals_rule_aux: actually use prems if present;
|
changeset |
files
|
| Sun, 26 Feb 2006 23:01:47 +0100 |
wenzelm |
add_local: do_index;
|
changeset |
files
|
| Sun, 26 Feb 2006 22:25:17 +0100 |
urbanc |
replaced the lemma at_two by at_different;
|
changeset |
files
|
| Sun, 26 Feb 2006 22:24:05 +0100 |
urbanc |
improved the decision-procedure for permutations;
|
changeset |
files
|
| Sat, 25 Feb 2006 15:19:47 +0100 |
haftmann |
improved codegen bootstrap
|
changeset |
files
|
| Sat, 25 Feb 2006 15:19:19 +0100 |
haftmann |
change in codegen syntax
|
changeset |
files
|
| Sat, 25 Feb 2006 15:19:00 +0100 |
haftmann |
some refinements
|
changeset |
files
|
| Sat, 25 Feb 2006 15:11:35 +0100 |
haftmann |
added more detailed data to consts
|
changeset |
files
|
| Fri, 24 Feb 2006 17:48:17 +0100 |
berghofe |
Reverted to old interface of AxClass.add_inst_arity(_i)
|
changeset |
files
|
| Fri, 24 Feb 2006 09:00:21 +0100 |
berghofe |
Adapted to Florian's recent changes to the AxClass package.
|
changeset |
files
|
| Thu, 23 Feb 2006 20:56:31 +0100 |
urbanc |
added lemmas
|
changeset |
files
|
| Thu, 23 Feb 2006 13:37:46 +0100 |
wenzelm |
make SML/NJ happy;
|
changeset |
files
|
| Thu, 23 Feb 2006 13:00:18 +0100 |
mengj |
Default type level is T_FULL now.
|
changeset |
files
|
| Thu, 23 Feb 2006 12:59:01 +0100 |
mengj |
eprover removes tmp files too.
|
changeset |
files
|
| Thu, 23 Feb 2006 12:57:39 +0100 |
mengj |
vampire/eprover methods can now be applied repeatedly until they fail.
|
changeset |
files
|
| Wed, 22 Feb 2006 22:18:42 +0100 |
wenzelm |
removed obsolete meta_conjunction_tr';
|
changeset |
files
|
| Wed, 22 Feb 2006 22:18:41 +0100 |
wenzelm |
rew: handle conjunctionI/D1/D2;
|
changeset |
files
|
| Wed, 22 Feb 2006 22:18:39 +0100 |
wenzelm |
simplified Pure conjunction, based on actual const;
|
changeset |
files
|
| Wed, 22 Feb 2006 22:18:38 +0100 |
wenzelm |
removed rename_indexes_wrt;
|
changeset |
files
|
| Wed, 22 Feb 2006 22:18:36 +0100 |
wenzelm |
renamed class_axms to class_intros;
|
changeset |
files
|
| Wed, 22 Feb 2006 22:18:33 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 22 Feb 2006 22:18:32 +0100 |
wenzelm |
simplified Pure conjunction;
|
changeset |
files
|
| Wed, 22 Feb 2006 22:18:31 +0100 |
wenzelm |
not_equal: replaced syntax translation by abbreviation;
|
changeset |
files
|
| Wed, 22 Feb 2006 10:18:17 +0100 |
haftmann |
abandoned merge_alists' in favour of generic AList.merge
|
changeset |
files
|
| Tue, 21 Feb 2006 16:37:54 +0100 |
nipkow |
added Tools/nbe, fixes
|
changeset |
files
|
| Tue, 21 Feb 2006 16:37:33 +0100 |
nipkow |
added Tools/nbe
|
changeset |
files
|
| Tue, 21 Feb 2006 16:18:50 +0100 |
nipkow |
New normalization-by-evaluation package
|
changeset |
files
|
| Tue, 21 Feb 2006 15:06:50 +0100 |
wenzelm |
distinct (op =);
|
changeset |
files
|
| Mon, 20 Feb 2006 21:51:50 +0100 |
kleing |
fixed
|
changeset |
files
|
| Mon, 20 Feb 2006 16:23:38 +0100 |
paulson |
Inclusion of subset_refl in ATP calls
|
changeset |
files
|
| Mon, 20 Feb 2006 16:22:52 +0100 |
paulson |
Fix variable-naming bug (?) by removing a needless recursive call
|
changeset |
files
|
| Mon, 20 Feb 2006 11:38:06 +0100 |
haftmann |
slight code generator serialization improvements
|
changeset |
files
|
| Mon, 20 Feb 2006 11:37:18 +0100 |
haftmann |
moved intro_classes from AxClass to ClassPackage
|
changeset |
files
|
| Sun, 19 Feb 2006 22:40:18 +0100 |
kleing |
fixed document
|
changeset |
files
|
| Sun, 19 Feb 2006 22:12:30 +0100 |
kleing |
* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
|
changeset |
files
|
| Sun, 19 Feb 2006 17:18:39 +0100 |
urbanc |
added a few lemmas to do with permutation-equivalence for the
|
changeset |
files
|
| Sun, 19 Feb 2006 13:21:32 +0100 |
kleing |
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
|
changeset |
files
|
| Sun, 19 Feb 2006 02:11:27 +0100 |
huffman |
use minimal imports
|
changeset |
files
|
| Sun, 19 Feb 2006 01:40:13 +0100 |
huffman |
use qualified name for return
|
changeset |
files
|
| Sat, 18 Feb 2006 18:08:23 +0100 |
wenzelm |
dest_def: tuned error msg;
|
changeset |
files
|
| Fri, 17 Feb 2006 20:03:21 +0100 |
wenzelm |
const constraints: provide TFrees instead of TVars,
|
changeset |
files
|
| Fri, 17 Feb 2006 20:03:19 +0100 |
wenzelm |
checkpoint/copy_node: reset body context;
|
changeset |
files
|
| Fri, 17 Feb 2006 20:03:17 +0100 |
wenzelm |
global_qeds: transfer body context;
|
changeset |
files
|
| Fri, 17 Feb 2006 20:03:14 +0100 |
wenzelm |
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
|
changeset |
files
|
| Fri, 17 Feb 2006 20:03:10 +0100 |
wenzelm |
constrain: assert const declaration, optional type (i.e. may delete constraints);
|
changeset |
files
|
| Fri, 17 Feb 2006 17:00:33 +0100 |
wenzelm |
removed Import/lazy_scan.ML;
|
changeset |
files
|
| Fri, 17 Feb 2006 15:43:46 +0100 |
paulson |
hyperlinks in the PDF work now
|
changeset |
files
|
| Fri, 17 Feb 2006 15:03:26 +0100 |
obua |
replaced Symbol.explode by explode
|
changeset |
files
|
| Fri, 17 Feb 2006 08:42:41 +0100 |
haftmann |
updated mailing list archive link
|
changeset |
files
|
| Fri, 17 Feb 2006 03:30:50 +0100 |
obua |
use monomorphic sequences / scanners
|
changeset |
files
|
| Fri, 17 Feb 2006 01:46:38 +0100 |
huffman |
make maybe into a real type constructor; remove monad syntax
|
changeset |
files
|
| Thu, 16 Feb 2006 23:40:32 +0100 |
obua |
use VectorScannerSeq instead of ListScannerSeq in xml.ML
|
changeset |
files
|
| Thu, 16 Feb 2006 23:31:32 +0100 |
obua |
removed lazy_scan
|
changeset |
files
|
| Thu, 16 Feb 2006 23:30:47 +0100 |
obua |
improved scanning
|
changeset |
files
|
| Thu, 16 Feb 2006 21:15:38 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Feb 2006 21:12:03 +0100 |
wenzelm |
Abstract Natural Numbers with polymorphic recursion.
|
changeset |
files
|
| Thu, 16 Feb 2006 21:12:00 +0100 |
wenzelm |
new-style definitions/abbreviations;
|
changeset |
files
|
| Thu, 16 Feb 2006 21:11:58 +0100 |
wenzelm |
added ex/Abstract_NAT.thy;
|
changeset |
files
|
| Thu, 16 Feb 2006 19:39:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Feb 2006 19:10:47 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:59:39 +0100 |
haftmann |
removed silly stuff
|
changeset |
files
|
| Thu, 16 Feb 2006 18:39:48 +0100 |
wenzelm |
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
|
changeset |
files
|
| Thu, 16 Feb 2006 18:26:04 +0100 |
wenzelm |
added abbreviation(_i);
|
changeset |
files
|
| Thu, 16 Feb 2006 18:26:03 +0100 |
wenzelm |
added put_thms_internal: local_naming, no fact index;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:26:02 +0100 |
wenzelm |
added put_thms_internal;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:26:01 +0100 |
wenzelm |
added abbrev element;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:26:00 +0100 |
wenzelm |
added 'abbreviation';
|
changeset |
files
|
| Thu, 16 Feb 2006 18:25:58 +0100 |
wenzelm |
added premsN;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:25:58 +0100 |
wenzelm |
Proof.put_thms_internal;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:25:56 +0100 |
wenzelm |
removed pointless replace;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:25:55 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:25:55 +0100 |
wenzelm |
dest_def: actually return beta-eta contracted equation;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:25:54 +0100 |
wenzelm |
derived specifications: definition, abbreviation, axiomatization;
|
changeset |
files
|
| Thu, 16 Feb 2006 18:25:52 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 16 Feb 2006 14:59:57 +0100 |
obua |
cache improvements
|
changeset |
files
|
| Thu, 16 Feb 2006 04:17:19 +0100 |
obua |
variable counter is now also cached
|
changeset |
files
|
| Thu, 16 Feb 2006 03:23:57 +0100 |
obua |
adapted to kernel changes
|
changeset |
files
|
| Thu, 16 Feb 2006 00:09:46 +0100 |
wenzelm |
tuned subst_bound(s);
|
changeset |
files
|
| Wed, 15 Feb 2006 23:57:06 +0100 |
obua |
fixed bugs, added caching
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:13 +0100 |
wenzelm |
added cases_node;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:12 +0100 |
wenzelm |
replaced qualified_force_prefix to sticky_prefix;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:11 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:11 +0100 |
wenzelm |
check_text: Toplevel.node option;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:09 +0100 |
wenzelm |
init/exit no longer change the theory (no naming);
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:09 +0100 |
wenzelm |
evaluate antiquotes depending on Toplevel.node option;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:07 +0100 |
wenzelm |
simplified presentation commands;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:06 +0100 |
wenzelm |
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:06 +0100 |
wenzelm |
removed qualified_force_prefix;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:04 +0100 |
wenzelm |
replaced qualified_force_prefix to sticky_prefix;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:04 +0100 |
wenzelm |
chop is no longer pervasive;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:02 +0100 |
wenzelm |
rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:02 +0100 |
wenzelm |
added distinct_prems_rl;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:35:00 +0100 |
wenzelm |
specifications_of: avoid partiality;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:34:59 +0100 |
wenzelm |
counter example: avoid vacuous trace;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:34:59 +0100 |
wenzelm |
cannot use section before setup;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:34:57 +0100 |
wenzelm |
used Tactic.distinct_subgoals_tac;
|
changeset |
files
|
| Wed, 15 Feb 2006 21:34:55 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
changeset |
files
|
| Wed, 15 Feb 2006 19:11:10 +0100 |
urbanc |
added lemma pt_perm_compose'
|
changeset |
files
|
| Wed, 15 Feb 2006 19:01:09 +0100 |
nipkow |
got rid of superfluous linorder_neqE-instance for int.
|
changeset |
files
|
| Wed, 15 Feb 2006 18:10:09 +0100 |
webertj |
typo in a comment fixed
|
changeset |
files
|
| Wed, 15 Feb 2006 17:09:45 +0100 |
haftmann |
exported some interfaces useful for other code generator approaches
|
changeset |
files
|
| Wed, 15 Feb 2006 17:09:25 +0100 |
haftmann |
some fixes
|
changeset |
files
|
| Wed, 15 Feb 2006 17:09:06 +0100 |
haftmann |
exported specifications_of
|
changeset |
files
|
| Tue, 14 Feb 2006 17:07:48 +0100 |
haftmann |
added theory of executable rational numbers
|
changeset |
files
|
| Tue, 14 Feb 2006 17:07:11 +0100 |
haftmann |
improved handling of iml abstractions
|
changeset |
files
|
| Tue, 14 Feb 2006 13:03:00 +0100 |
paulson |
fixed tracing
|
changeset |
files
|
| Mon, 13 Feb 2006 17:02:54 +0100 |
berghofe |
Adapted to Context.generic syntax.
|
changeset |
files
|
| Mon, 13 Feb 2006 14:05:43 +0100 |
mengj |
Fixed a bug of type unification.
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:28 +0100 |
wenzelm |
* ML/Pure/General: improved join interface for tables;
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:27 +0100 |
wenzelm |
consts: maintain thy version for efficient transfer;
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:25 +0100 |
wenzelm |
export exception SAME (for join);
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:24 +0100 |
wenzelm |
low-level tuning of merge: maintain identity of accesses;
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:23 +0100 |
wenzelm |
share exception UNDEF with Table;
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:22 +0100 |
wenzelm |
structure Datatab: private copy avoids potential conflict of table exceptions;
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:21 +0100 |
wenzelm |
added eq_consts;
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:20 +0100 |
wenzelm |
minor tuning of proofs, notably induct;
|
changeset |
files
|
| Sun, 12 Feb 2006 21:34:18 +0100 |
wenzelm |
simplified TableFun.join;
|
changeset |
files
|
| Sun, 12 Feb 2006 20:32:59 +0100 |
wenzelm |
\usepackage{amssymb};
|
changeset |
files
|
| Sun, 12 Feb 2006 12:29:01 +0100 |
kleing |
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
|
changeset |
files
|
| Sun, 12 Feb 2006 10:42:19 +0100 |
kleing |
* moved ThreeDivides from Isar_examples to better suited HOL/ex
|
changeset |
files
|
| Sun, 12 Feb 2006 04:31:18 +0100 |
kleing |
divisibility by 3 theorem, contributed by Benjamin Porter,
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:55 +0100 |
wenzelm |
replaced mixfix_conflict by mixfix_content;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:54 +0100 |
wenzelm |
added map_theory;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:53 +0100 |
wenzelm |
added abbreviations: activated by init, no expressions yet;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:52 +0100 |
wenzelm |
added restore;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:51 +0100 |
wenzelm |
tuned mixfixes, mixfix_conflict;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:50 +0100 |
wenzelm |
removed custom_accesses;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:49 +0100 |
wenzelm |
added variant_name;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:48 +0100 |
wenzelm |
removed custom_accesses;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:47 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 11 Feb 2006 17:17:45 +0100 |
wenzelm |
added chop (sane version of splitAt);
|
changeset |
files
|
| Sat, 11 Feb 2006 14:25:23 +0100 |
mengj |
Changed some code due to changes in reduce_axiomsN.ML.
|
changeset |
files
|
| Sat, 11 Feb 2006 14:23:35 +0100 |
mengj |
Added another filter strategy.
|
changeset |
files
|
| Fri, 10 Feb 2006 09:09:07 +0100 |
haftmann |
improved code generator devarification
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:59 +0100 |
wenzelm |
statement: improved error msg;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:57 +0100 |
wenzelm |
* ML/Pure: generic Args/Attrib syntax everywhere;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:56 +0100 |
wenzelm |
moved fixedN to lexicon.ML;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:54 +0100 |
wenzelm |
added mfix_delims;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:52 +0100 |
wenzelm |
added mixfix_conflict;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:50 +0100 |
wenzelm |
added fixedN, constN;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:48 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:46 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:43 +0100 |
wenzelm |
syntax: Context.generic;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:41 +0100 |
wenzelm |
Context.generic is canonical state of parsers;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:39 +0100 |
wenzelm |
Local syntax depending on theory syntax.
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:37 +0100 |
wenzelm |
decode: observe Syntax.constN;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:35 +0100 |
wenzelm |
removed obsolete add_typ/term_classes/tycons;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:32 +0100 |
wenzelm |
tuned extern_term, pretty_term';
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:29 +0100 |
wenzelm |
removed set quick_and_dirty and ThmDeps.enable -- no effect here;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:24 +0100 |
wenzelm |
abbrevs: store in reverted orientation;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:23 +0100 |
wenzelm |
use proof_general.ML: setmp quick_and_dirty captures default value;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:21 +0100 |
wenzelm |
added Isar/local_syntax.ML;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:19 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:16 +0100 |
wenzelm |
Args/Attrib syntax: Context.generic;
|
changeset |
files
|
| Fri, 10 Feb 2006 02:22:13 +0100 |
wenzelm |
simplified polyml example;
|
changeset |
files
|
| Thu, 09 Feb 2006 12:20:31 +0100 |
paulson |
tidying
|
changeset |
files
|
| Thu, 09 Feb 2006 12:20:02 +0100 |
paulson |
blacklist tweaks
|
changeset |
files
|
| Thu, 09 Feb 2006 12:14:39 +0100 |
paulson |
names for simprules
|
changeset |
files
|
| Thu, 09 Feb 2006 03:34:56 +0100 |
huffman |
removed redundant lemmas
|
changeset |
files
|
| Thu, 09 Feb 2006 03:01:11 +0100 |
huffman |
no longer need All_equiv lemmas
|
changeset |
files
|
| Wed, 08 Feb 2006 17:15:28 +0100 |
wenzelm |
map_type_tvar/tfree: map_atyps;
|
changeset |
files
|
| Wed, 08 Feb 2006 17:15:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 08 Feb 2006 15:17:54 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 08 Feb 2006 15:12:59 +0100 |
nipkow |
made "dvd" on numbers executable by simp.
|
changeset |
files
|
| Wed, 08 Feb 2006 14:39:00 +0100 |
haftmann |
introduced gen_distinct in place of distinct
|
changeset |
files
|
| Wed, 08 Feb 2006 09:27:20 +0100 |
haftmann |
fixed the most silly bug conceivable in map_atyps
|
changeset |
files
|
| Tue, 07 Feb 2006 19:57:00 +0100 |
wenzelm |
lambda: base name of Const;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:58 +0100 |
wenzelm |
adapted Sign.infer_types;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:57 +0100 |
wenzelm |
has_duplicates;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:56 +0100 |
wenzelm |
adapted Sign.infer_types;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:54 +0100 |
wenzelm |
added local consts component;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:53 +0100 |
wenzelm |
Library.is_equal;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:51 +0100 |
wenzelm |
removed obsolete sign_of_cterm;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:50 +0100 |
wenzelm |
adapted Sign.infer_types(_simult), Sign.certify_term/prop;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:49 +0100 |
wenzelm |
export consts_of;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:48 +0100 |
wenzelm |
removed eq-polymorphic duplicates;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:47 +0100 |
wenzelm |
renamed space to space_of;
|
changeset |
files
|
| Tue, 07 Feb 2006 19:56:45 +0100 |
wenzelm |
renamed gen_duplicates to duplicates;
|
changeset |
files
|
| Tue, 07 Feb 2006 08:47:43 +0100 |
haftmann |
slight improvements in code generation
|
changeset |
files
|
| Mon, 06 Feb 2006 21:02:01 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Mon, 06 Feb 2006 21:00:01 +0100 |
wenzelm |
Logic.combound;
|
changeset |
files
|
| Mon, 06 Feb 2006 21:00:00 +0100 |
wenzelm |
adapted Consts.dest;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:59 +0100 |
wenzelm |
Sign.cert_def;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:58 +0100 |
wenzelm |
added bound_vars;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:57 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:56 +0100 |
wenzelm |
Envir.(beta_)eta_contract;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:55 +0100 |
wenzelm |
added local_theory, with optional locale xname;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:54 +0100 |
wenzelm |
type local_theory;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:53 +0100 |
wenzelm |
norm_term: Sign.const_expansion, Envir.expand_atom;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:52 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:51 +0100 |
wenzelm |
type local_theory = Proof.context;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:50 +0100 |
wenzelm |
cert_def: use Logic.dest_def;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:49 +0100 |
wenzelm |
Toplevel.local_theory;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:48 +0100 |
wenzelm |
LocalDefs.cert_def;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:47 +0100 |
wenzelm |
eq_prop: Envir.beta_eta_contract;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:46 +0100 |
wenzelm |
renamed xxx_multi to xxx_list;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:42 +0100 |
wenzelm |
moved combound, rlist_abs to logic.ML;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:11 +0100 |
wenzelm |
union_tpairs: Library.merge;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:10 +0100 |
wenzelm |
moved no_vars to sign.ML;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:09 +0100 |
wenzelm |
lambda: abstract over any const;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:08 +0100 |
wenzelm |
added add_abbrevs(_i);
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:07 +0100 |
wenzelm |
moved (beta_)eta_contract to envir.ML;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:06 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:05 +0100 |
wenzelm |
added generic dest_def (mostly from theory.ML);
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:04 +0100 |
wenzelm |
added (beta_)eta_contract (from pattern.ML);
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:03 +0100 |
wenzelm |
print_theory: const abbreviations;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:02 +0100 |
wenzelm |
added abbreviations;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:01 +0100 |
wenzelm |
load envir.ML and logic.ML early;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:00 +0100 |
wenzelm |
Logic.rlist_abs;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:58:59 +0100 |
wenzelm |
Logic.const_of_class/class_of_const;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:58:57 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:58:56 +0100 |
wenzelm |
replaced Symtab.merge_multi by local merge_rules;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:58:54 +0100 |
wenzelm |
Envir.(beta_)eta_contract;
|
changeset |
files
|
| Mon, 06 Feb 2006 11:01:28 +0100 |
haftmann |
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
|
changeset |
files
|
| Mon, 06 Feb 2006 11:00:24 +0100 |
haftmann |
added strip_abs
|
changeset |
files
|
| Mon, 06 Feb 2006 11:00:06 +0100 |
haftmann |
clarified semantics of merge
|
changeset |
files
|
| Sat, 04 Feb 2006 03:14:32 +0100 |
huffman |
speedup: use simproc for AC rules
|
changeset |
files
|
| Sat, 04 Feb 2006 02:37:09 +0100 |
huffman |
UU_reorient_simproc no longer rewrites UU = numeral
|
changeset |
files
|
| Fri, 03 Feb 2006 23:12:31 +0100 |
wenzelm |
removed obsolete gen_ins/mem;
|
changeset |
files
|
| Fri, 03 Feb 2006 23:12:30 +0100 |
wenzelm |
removed add/del_rules;
|
changeset |
files
|
| Fri, 03 Feb 2006 23:12:28 +0100 |
wenzelm |
canonical member/insert/merge;
|
changeset |
files
|
| Fri, 03 Feb 2006 17:08:03 +0100 |
paulson |
removal of case analysis clauses
|
changeset |
files
|
| Fri, 03 Feb 2006 17:02:33 +0100 |
haftmann |
fix
|
changeset |
files
|
| Fri, 03 Feb 2006 11:48:11 +0100 |
haftmann |
minor improvements
|
changeset |
files
|
| Fri, 03 Feb 2006 11:47:57 +0100 |
haftmann |
refined signature of locale module
|
changeset |
files
|
| Fri, 03 Feb 2006 08:48:33 +0100 |
haftmann |
no toplevel 'thy' anymore
|
changeset |
files
|
| Fri, 03 Feb 2006 08:48:16 +0100 |
haftmann |
fix in codegen
|
changeset |
files
|
| Thu, 02 Feb 2006 21:59:55 +0100 |
wenzelm |
do not open structure;
|
changeset |
files
|
| Thu, 02 Feb 2006 19:57:13 +0100 |
huffman |
reimplemented using Equiv_Relations.thy
|
changeset |
files
|
| Thu, 02 Feb 2006 18:04:10 +0100 |
haftmann |
improvement in devarifications
|
changeset |
files
|
| Thu, 02 Feb 2006 18:03:35 +0100 |
haftmann |
alternative syntax for instances
|
changeset |
files
|
| Thu, 02 Feb 2006 16:37:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:38 +0100 |
wenzelm |
consumes: negative argument relative to total number of prems;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:37 +0100 |
wenzelm |
added refine_insert;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:35 +0100 |
wenzelm |
Proof.refine_insert;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:34 +0100 |
wenzelm |
always use Attrib.src;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:33 +0100 |
wenzelm |
more generic type for map_specs/facts;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:32 +0100 |
wenzelm |
'obtains' element;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:31 +0100 |
wenzelm |
'obtain': optional case name;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:30 +0100 |
wenzelm |
index elements;
|
changeset |
files
|
| Thu, 02 Feb 2006 16:31:28 +0100 |
wenzelm |
* Isar: 'obtains' element;
|
changeset |
files
|
| Thu, 02 Feb 2006 12:54:24 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Thu, 02 Feb 2006 12:54:08 +0100 |
wenzelm |
theorem(_in_locale): Element.statement, Obtain.statement;
|
changeset |
files
|
| Thu, 02 Feb 2006 12:52:25 +0100 |
wenzelm |
added parname;
|
changeset |
files
|
| Thu, 02 Feb 2006 12:52:24 +0100 |
wenzelm |
obtain(_i): optional name for 'that';
|
changeset |
files
|
| Thu, 02 Feb 2006 12:52:21 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 02 Feb 2006 12:52:20 +0100 |
wenzelm |
moved (general_)statement to outer_parse.ML;
|
changeset |
files
|
| Thu, 02 Feb 2006 12:52:19 +0100 |
wenzelm |
added concluding statements: Shows/Obtains;
|
changeset |
files
|
| Thu, 02 Feb 2006 12:52:18 +0100 |
wenzelm |
moved specific map_typ/term to sign.ML;
|
changeset |
files
|
| Thu, 02 Feb 2006 12:52:16 +0100 |
wenzelm |
added specific map_typ/term (from term.ML);
|
changeset |
files
|
| Thu, 02 Feb 2006 10:24:06 +0100 |
krauss |
Exporting recdef's hints for use by new recdef package
|
changeset |
files
|
| Thu, 02 Feb 2006 10:12:45 +0100 |
ballarin |
*_asms_of fixed.
|
changeset |
files
|
| Thu, 02 Feb 2006 02:02:00 +0100 |
kleing |
add 64bit atbroy98 platform
|
changeset |
files
|
| Wed, 01 Feb 2006 22:20:40 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 01 Feb 2006 19:19:32 +0100 |
berghofe |
Added "evaluation" method and oracle.
|
changeset |
files
|
| Wed, 01 Feb 2006 15:22:02 +0100 |
paulson |
new and updated protocol proofs by Giamp Bella
|
changeset |
files
|
| Wed, 01 Feb 2006 12:23:14 +0100 |
haftmann |
substantial cleanup and simplifications
|
changeset |
files
|
| Wed, 01 Feb 2006 12:22:47 +0100 |
haftmann |
name clarifications
|
changeset |
files
|
| Wed, 01 Feb 2006 12:22:19 +0100 |
haftmann |
added map_entry_yield
|
changeset |
files
|
| Wed, 01 Feb 2006 01:05:17 +0100 |
urbanc |
- renamed some lemmas (some had names coming from ancient
|
changeset |
files
|
| Wed, 01 Feb 2006 01:03:41 +0100 |
urbanc |
added all constructors from PhD
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:36 +0100 |
wenzelm |
axiomatization: retrict parameters to occurrences in specs;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:35 +0100 |
wenzelm |
improved comments;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:34 +0100 |
wenzelm |
tuned LocalDefs.unfold;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:32 +0100 |
wenzelm |
(un)fold: removed '(raw)' option;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:31 +0100 |
wenzelm |
added consts_retricted;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:30 +0100 |
wenzelm |
(un)fold: no raw flag;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:28 +0100 |
wenzelm |
tuned LocalTheory.pretty_consts;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:27 +0100 |
wenzelm |
(un)folded: removed '(raw)' option;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:26 +0100 |
wenzelm |
lambda: abstract over TYPE argument, too;
|
changeset |
files
|
| Tue, 31 Jan 2006 18:19:25 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 31 Jan 2006 17:48:28 +0100 |
paulson |
removal of ResClause.num_of_clauses and other simplifications
|
changeset |
files
|
| Tue, 31 Jan 2006 16:37:06 +0100 |
paulson |
working SPASS support; much tidying
|
changeset |
files
|
| Tue, 31 Jan 2006 16:26:18 +0100 |
haftmann |
added serialization for arbitrary
|
changeset |
files
|
| Tue, 31 Jan 2006 16:15:51 +0100 |
haftmann |
minor change to CodegenPackage interface
|
changeset |
files
|
| Tue, 31 Jan 2006 16:14:37 +0100 |
haftmann |
minor cleanups
|
changeset |
files
|
| Tue, 31 Jan 2006 16:12:56 +0100 |
haftmann |
more coherent lookup extraction functions
|
changeset |
files
|
| Tue, 31 Jan 2006 10:39:13 +0100 |
paulson |
reorganization of code to support DFG otuput
|
changeset |
files
|
| Tue, 31 Jan 2006 00:51:15 +0100 |
wenzelm |
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
|
changeset |
files
|
| Tue, 31 Jan 2006 00:43:14 +0100 |
wenzelm |
declare defn rules;
|
changeset |
files
|
| Tue, 31 Jan 2006 00:39:44 +0100 |
wenzelm |
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
|
changeset |
files
|
| Tue, 31 Jan 2006 00:39:43 +0100 |
wenzelm |
export meta_rewrite_rule;
|
changeset |
files
|
| Tue, 31 Jan 2006 00:39:43 +0100 |
wenzelm |
advanced translations: Context.generic;
|
changeset |
files
|
| Tue, 31 Jan 2006 00:39:40 +0100 |
wenzelm |
advanced translations: Context.generic;
|
changeset |
files
|
| Mon, 30 Jan 2006 15:31:31 +0100 |
paulson |
tidy-up of res_clause.ML, removing the "predicates" field
|
changeset |
files
|
| Mon, 30 Jan 2006 12:20:06 +0100 |
wenzelm |
'setup': no list type, support implicit setup;
|
changeset |
files
|
| Mon, 30 Jan 2006 12:20:05 +0100 |
wenzelm |
'fixes': support plain vars;
|
changeset |
files
|
| Mon, 30 Jan 2006 10:13:28 +0100 |
paulson |
fixed a syntax error!
|
changeset |
files
|
| Mon, 30 Jan 2006 08:47:38 +0100 |
haftmann |
replaced gen_list by enum
|
changeset |
files
|
| Mon, 30 Jan 2006 08:20:56 +0100 |
haftmann |
adaptions to codegen_package
|
changeset |
files
|
| Mon, 30 Jan 2006 08:20:06 +0100 |
haftmann |
various improvements
|
changeset |
files
|
| Mon, 30 Jan 2006 08:19:30 +0100 |
haftmann |
added three times overloaded Isar instance command
|
changeset |
files
|
| Mon, 30 Jan 2006 08:18:51 +0100 |
haftmann |
moved instance Isar command to class_package.ML
|
changeset |
files
|
| Mon, 30 Jan 2006 08:17:04 +0100 |
haftmann |
added map_atype, map_aterms
|
changeset |
files
|
| Sun, 29 Jan 2006 19:24:56 +0100 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:52 +0100 |
wenzelm |
declare atomize/defn for Ball;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:51 +0100 |
wenzelm |
invent_fixes: merely enter body temporarily;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:50 +0100 |
wenzelm |
'unfolding': LocalDefs.unfold;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:49 +0100 |
wenzelm |
moved treatment of object-logic equalities to local_defs.ML;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:48 +0100 |
wenzelm |
method (un)folded: option '(raw)';
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:47 +0100 |
wenzelm |
added attributes defn_add/del;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:46 +0100 |
wenzelm |
added 'defn' attribute;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:45 +0100 |
wenzelm |
proper order of trfuns;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:44 +0100 |
wenzelm |
CPure: Context.add_setup;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:43 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:42 +0100 |
wenzelm |
implicit setup;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:41 +0100 |
wenzelm |
default rule step: norm_hhf_tac;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:40 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sun, 29 Jan 2006 19:23:38 +0100 |
wenzelm |
declare 'defn' rules;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:29:49 +0100 |
wenzelm |
LocalDefs;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:29:06 +0100 |
wenzelm |
Basic operations on local definitions.
|
changeset |
files
|
| Sat, 28 Jan 2006 17:29:04 +0100 |
wenzelm |
removed unnecessary Syntax.fix_mixfix;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:29:03 +0100 |
wenzelm |
added axiomatization_loc, definition_loc;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:29:02 +0100 |
wenzelm |
moved local defs to local_defs.ML;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:29:00 +0100 |
wenzelm |
LocalDefs;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:59 +0100 |
wenzelm |
removed unatomize;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:58 +0100 |
wenzelm |
(un)fold: support object-level rewrites;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:57 +0100 |
wenzelm |
added print_consts;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:56 +0100 |
wenzelm |
removed obsolete keyword 'files';
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:55 +0100 |
wenzelm |
(un)folded: support object-level rewrites;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:54 +0100 |
wenzelm |
added equals_cong;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:53 +0100 |
wenzelm |
added Isar/local_defs.ML;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:52 +0100 |
wenzelm |
LocalDefs.add_def;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:51 +0100 |
wenzelm |
LocalDefs.def_export;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:50 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 28 Jan 2006 17:28:48 +0100 |
wenzelm |
Pure/Isar: (un)folded, (un)fold, unfolding support
|
changeset |
files
|
| Fri, 27 Jan 2006 20:17:24 +0100 |
webertj |
interrupt_timeout for Poly replaced by stub
|
changeset |
files
|
| Fri, 27 Jan 2006 19:05:24 +0100 |
wenzelm |
added atomize_iff;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:19 +0100 |
wenzelm |
renamed Pretty.gen_list to Pretty.enum;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:17 +0100 |
wenzelm |
swapped theory_context;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:16 +0100 |
wenzelm |
swapped Toplevel.theory_context;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:15 +0100 |
wenzelm |
added invent_fixes;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:14 +0100 |
wenzelm |
swapped Toplevel.theory_context;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:13 +0100 |
wenzelm |
renamed reverse_atomize to unatomize;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:12 +0100 |
wenzelm |
init: include view;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:11 +0100 |
wenzelm |
improved 'notes', including proper treatment of locale results;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:10 +0100 |
wenzelm |
swapped Toplevel.theory_context;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:09 +0100 |
wenzelm |
Locale.init;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:08 +0100 |
wenzelm |
renamed gen_list to enum;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:07 +0100 |
wenzelm |
moved theorem tags from Drule to PureThy;
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:05 +0100 |
wenzelm |
added ProofContext.pprint_context (depends on ProofContext.debug);
|
changeset |
files
|
| Fri, 27 Jan 2006 19:03:02 +0100 |
wenzelm |
moved theorem tags from Drule to PureThy;
|
changeset |
files
|
| Fri, 27 Jan 2006 18:29:33 +0100 |
paulson |
tidying up SPASS output
|
changeset |
files
|
| Fri, 27 Jan 2006 18:29:11 +0100 |
paulson |
tidying
|
changeset |
files
|
| Fri, 27 Jan 2006 18:28:55 +0100 |
paulson |
better reporting
|
changeset |
files
|
| Fri, 27 Jan 2006 16:05:23 +0100 |
ballarin |
Interface to access the specification of a named locale.
|
changeset |
files
|
| Fri, 27 Jan 2006 05:46:39 +0100 |
mengj |
Added new file Tools/ATP/reduce_axiomsN.ML
|
changeset |
files
|
| Fri, 27 Jan 2006 05:45:25 +0100 |
mengj |
Added in new file Tools/ATP/reduce_axiomsN.ML
|
changeset |
files
|
| Fri, 27 Jan 2006 05:37:12 +0100 |
mengj |
Changed codes that call relevance filter.
|
changeset |
files
|
| Fri, 27 Jan 2006 05:34:20 +0100 |
mengj |
Relevance filtering. Has replaced the previous version.
|
changeset |
files
|
| Thu, 26 Jan 2006 20:42:15 +0100 |
webertj |
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
|
changeset |
files
|
| Thu, 26 Jan 2006 20:17:54 +0100 |
webertj |
smaller example to prevent timeout
|
changeset |
files
|
| Thu, 26 Jan 2006 17:58:01 +0100 |
berghofe |
Fixed bug in code generator for primitive definitions that
|
changeset |
files
|
| Thu, 26 Jan 2006 15:37:14 +0100 |
berghofe |
Inductive sets with no introduction rules are now allowed as well.
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:44 +0100 |
wenzelm |
added definition(_i);
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:43 +0100 |
wenzelm |
renamed export to export_standard (again!), because it includes Drule.local_standard';
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:42 +0100 |
wenzelm |
ProofContext.export_standard;
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:41 +0100 |
wenzelm |
tuned atomize_cterm;
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:40 +0100 |
wenzelm |
turned abstract_term into ProofContext.abs_def;
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:39 +0100 |
wenzelm |
added constant definition;
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:38 +0100 |
wenzelm |
added 'definition';
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:37 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:36 +0100 |
wenzelm |
export name_multi;
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:35 +0100 |
wenzelm |
abs_def: improved error;
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:34 +0100 |
wenzelm |
ObjectLogic.atomize_cterm;
|
changeset |
files
|
| Wed, 25 Jan 2006 00:21:32 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 24 Jan 2006 15:16:06 +0100 |
webertj |
works with DPLL solver now
|
changeset |
files
|
| Tue, 24 Jan 2006 13:28:06 +0100 |
urbanc |
the additional freshness-condition in the one-induction
|
changeset |
files
|
| Tue, 24 Jan 2006 00:44:39 +0100 |
wenzelm |
fixed code_generate syntax;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:34 +0100 |
wenzelm |
renamed axiomatize(_i) to axiomatization(_i);
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:33 +0100 |
wenzelm |
renamed inferred_type to inferred_param;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:32 +0100 |
wenzelm |
ProofContext.inferred_param;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:31 +0100 |
wenzelm |
removed the_params;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:29 +0100 |
wenzelm |
added actual operations;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:28 +0100 |
wenzelm |
axiomatization: optional vars;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:27 +0100 |
wenzelm |
LocalTheory.pretty_consts;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:25 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:24 +0100 |
wenzelm |
add_finals: prep_consts, i.e. varify type;
|
changeset |
files
|
| Tue, 24 Jan 2006 00:43:23 +0100 |
wenzelm |
added dest_all;
|
changeset |
files
|
| Mon, 23 Jan 2006 18:20:48 +0100 |
webertj |
TimeLimit replaced by interrupt_timeout
|
changeset |
files
|
| Mon, 23 Jan 2006 17:29:52 +0100 |
webertj |
TimeLimit replaced by interrupt_timeout
|
changeset |
files
|
| Mon, 23 Jan 2006 15:23:31 +0100 |
krauss |
Updated to Isabelle 2006-01-23
|
changeset |
files
|
| Mon, 23 Jan 2006 15:14:06 +0100 |
urbanc |
made change for ex1
|
changeset |
files
|
| Mon, 23 Jan 2006 14:07:52 +0100 |
haftmann |
removed problematic keyword 'atom'
|
changeset |
files
|
| Mon, 23 Jan 2006 14:06:40 +0100 |
haftmann |
more general serializer
|
changeset |
files
|
| Mon, 23 Jan 2006 14:06:28 +0100 |
haftmann |
slight steps forward
|
changeset |
files
|
| Mon, 23 Jan 2006 14:06:11 +0100 |
haftmann |
exported after_qed for axclass instance
|
changeset |
files
|
| Mon, 23 Jan 2006 11:41:54 +0100 |
paulson |
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
|
changeset |
files
|
| Mon, 23 Jan 2006 11:38:43 +0100 |
paulson |
Clausification now handles some IFs in rewrite rules (if-split did not work)
|
changeset |
files
|
| Mon, 23 Jan 2006 11:37:53 +0100 |
paulson |
bugfix: induct_tac no longer raises THM "dest_state"
|
changeset |
files
|
| Mon, 23 Jan 2006 11:36:50 +0100 |
paulson |
fixed the <<= notation
|
changeset |
files
|
| Mon, 23 Jan 2006 11:36:05 +0100 |
paulson |
replacement of bool by a datatype (making problems first-order). More lemma names
|
changeset |
files
|
| Mon, 23 Jan 2006 10:34:38 +0100 |
mengj |
Fixed a bug.
|
changeset |
files
|
| Sun, 22 Jan 2006 22:16:34 +0100 |
urbanc |
no essential changes
|
changeset |
files
|
| Sun, 22 Jan 2006 22:11:50 +0100 |
urbanc |
made the change for setup-functions not returning functions
|
changeset |
files
|
| Sun, 22 Jan 2006 21:58:43 +0100 |
urbanc |
a fixme comments about abs_fun_if, which should be called perm_if
|
changeset |
files
|
| Sun, 22 Jan 2006 18:46:01 +0100 |
wenzelm |
Local theory operations, with optional target locale.
|
changeset |
files
|
| Sun, 22 Jan 2006 18:46:00 +0100 |
wenzelm |
added restore_body;
|
changeset |
files
|
| Sun, 22 Jan 2006 18:45:59 +0100 |
wenzelm |
added the_params;
|
changeset |
files
|
| Sun, 22 Jan 2006 18:45:58 +0100 |
wenzelm |
tuned order;
|
changeset |
files
|
| Sun, 22 Jan 2006 18:45:57 +0100 |
wenzelm |
added Isar/local_theory.ML;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:22:40 +0100 |
mengj |
Ensure dereference is delayed.
|
changeset |
files
|
| Sat, 21 Jan 2006 23:07:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:30 +0100 |
wenzelm |
* ML: simplified type attribute;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:29 +0100 |
wenzelm |
simplified type attribute;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:28 +0100 |
wenzelm |
removed duplicate type_solver (cf. Tools/typechk.ML);
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:27 +0100 |
wenzelm |
simplified type attribute;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:25 +0100 |
wenzelm |
simplified type attribute;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:24 +0100 |
wenzelm |
simplified type attribute;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:23 +0100 |
wenzelm |
rename map_theory/proof to theory/proof_map;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:21 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:20 +0100 |
wenzelm |
simplified type attribute;
|
changeset |
files
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
changeset |
files
|
| Fri, 20 Jan 2006 04:53:59 +0100 |
mengj |
type information is now also printed.
|
changeset |
files
|
| Fri, 20 Jan 2006 04:50:01 +0100 |
mengj |
added some debugging code.
|
changeset |
files
|
| Fri, 20 Jan 2006 04:35:23 +0100 |
mengj |
fixed a bug
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:30 +0100 |
wenzelm |
quote "atom";
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:29 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:27 +0100 |
wenzelm |
* ML/Isar: theory setup has type (theory -> theory);
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:26 +0100 |
wenzelm |
use/use_thy: Output.toplevel_errors;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:25 +0100 |
wenzelm |
added basic syntax;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:24 +0100 |
wenzelm |
moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:23 +0100 |
wenzelm |
keep: disable Output.toplevel_errors;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:22 +0100 |
wenzelm |
run_thy: removed Output.toplevel_errors;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:21 +0100 |
wenzelm |
added ML_errors;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:20 +0100 |
wenzelm |
use: Output.ML_errors;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:19 +0100 |
wenzelm |
Syntax.basic_syn;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:18 +0100 |
wenzelm |
setup: theory -> theory;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:17 +0100 |
wenzelm |
tuned setmp;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:16 +0100 |
wenzelm |
setup: theory -> theory;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:15 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:14 +0100 |
wenzelm |
setup: theory -> theory;
|
changeset |
files
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
changeset |
files
|
| Thu, 19 Jan 2006 15:45:10 +0100 |
berghofe |
Use generic Simplifier.simp_add attribute instead
|
changeset |
files
|
| Thu, 19 Jan 2006 14:59:55 +0100 |
berghofe |
Re-inserted consts_code declaration accidentally deleted
|
changeset |
files
|
| Thu, 19 Jan 2006 10:22:13 +0100 |
paulson |
strengthened some lemmas; simplified some proofs
|
changeset |
files
|
| Wed, 18 Jan 2006 11:55:50 +0100 |
haftmann |
substantial improvement in serialization handling
|
changeset |
files
|
| Wed, 18 Jan 2006 02:48:58 +0100 |
urbanc |
fixed one proof that broke because of the changes
|
changeset |
files
|
| Tue, 17 Jan 2006 16:36:57 +0100 |
haftmann |
substantial improvements in code generator
|
changeset |
files
|
| Tue, 17 Jan 2006 10:26:50 +0100 |
paulson |
these hacks are no longer needed
|
changeset |
files
|
| Tue, 17 Jan 2006 10:26:36 +0100 |
paulson |
improved SPASS support
|
changeset |
files
|
| Mon, 16 Jan 2006 21:55:17 +0100 |
wenzelm |
case_result: drop_schematic, i.e. be permissive about illegal binds;
|
changeset |
files
|
| Mon, 16 Jan 2006 21:55:15 +0100 |
wenzelm |
put_facts: do not pretend local thms were named;
|
changeset |
files
|
| Mon, 16 Jan 2006 21:55:14 +0100 |
wenzelm |
declare the1_equality [elim?];
|
changeset |
files
|
| Sun, 15 Jan 2006 20:04:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 15 Jan 2006 20:00:59 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 15 Jan 2006 19:58:57 +0100 |
wenzelm |
* Classical: optional weight for attributes;
|
changeset |
files
|
| Sun, 15 Jan 2006 19:58:56 +0100 |
wenzelm |
guess: used fixed inferred_type of vars;
|
changeset |
files
|
| Sun, 15 Jan 2006 19:58:55 +0100 |
wenzelm |
export add_args;
|
changeset |
files
|
| Sun, 15 Jan 2006 19:58:54 +0100 |
wenzelm |
attributes: optional weight;
|
changeset |
files
|
| Sun, 15 Jan 2006 19:58:53 +0100 |
wenzelm |
classical attributes: optional weight;
|
changeset |
files
|
| Sun, 15 Jan 2006 19:58:51 +0100 |
wenzelm |
prefer ex1I over ex_ex1I in single-step reasoning;
|
changeset |
files
|
| Sat, 14 Jan 2006 22:25:34 +0100 |
wenzelm |
generic attributes;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:20:51 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:15:24 +0100 |
wenzelm |
* ML/Isar: simplified treatment of user-level errors;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:14:18 +0100 |
wenzelm |
sane ERROR vs. TOPLEVEL_ERROR handling;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:14:17 +0100 |
wenzelm |
added Isar.toplevel;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:14:16 +0100 |
wenzelm |
Output.error_msg;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:14:15 +0100 |
wenzelm |
removed special ERROR handling stuff (transform_error etc.);
|
changeset |
files
|
| Sat, 14 Jan 2006 17:14:14 +0100 |
wenzelm |
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:14:13 +0100 |
wenzelm |
Output.debug;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:14:11 +0100 |
wenzelm |
generated code: raise Match instead of ERROR;
|
changeset |
files
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
changeset |
files
|
| Fri, 13 Jan 2006 17:39:41 +0100 |
paulson |
blacklist experiments
|
changeset |
files
|
| Fri, 13 Jan 2006 17:39:19 +0100 |
paulson |
more readable divide ops
|
changeset |
files
|
| Fri, 13 Jan 2006 17:39:03 +0100 |
paulson |
more practical time limit
|
changeset |
files
|
| Fri, 13 Jan 2006 14:43:09 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:17 +0100 |
wenzelm |
mixfix: added Structure;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:16 +0100 |
wenzelm |
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:15 +0100 |
wenzelm |
uniform handling of fixes;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:11 +0100 |
wenzelm |
uniform handling of fixes;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:08 +0100 |
wenzelm |
uniform handling of fixes;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:06 +0100 |
wenzelm |
uniform handling of fixes;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:03 +0100 |
wenzelm |
generic_setup: optional argument, defaults to Context.setup();
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:02 +0100 |
wenzelm |
added map_theory, map_proof;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:13:00 +0100 |
wenzelm |
removed obsolete sign_of;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:12:59 +0100 |
wenzelm |
implicit setup, which admits exception_trace;
|
changeset |
files
|
| Fri, 13 Jan 2006 01:12:58 +0100 |
wenzelm |
ProofContext.def_export;
|
changeset |
files
|
| Wed, 11 Jan 2006 18:46:31 +0100 |
urbanc |
updated to new induction principle
|
changeset |
files
|
| Wed, 11 Jan 2006 18:39:19 +0100 |
urbanc |
cahges to use the new induction-principle (now proved in
|
changeset |
files
|
| Wed, 11 Jan 2006 18:38:32 +0100 |
urbanc |
changes to make use of the new induction principle proved by
|
changeset |
files
|
| Wed, 11 Jan 2006 18:21:23 +0100 |
berghofe |
Implemented proof of (strong) induction rule.
|
changeset |
files
|
| Wed, 11 Jan 2006 18:20:59 +0100 |
berghofe |
Added theorem at_finite_select.
|
changeset |
files
|
| Wed, 11 Jan 2006 17:12:30 +0100 |
urbanc |
added lemmas perm_empty, perm_insert to do with
|
changeset |
files
|
| Wed, 11 Jan 2006 17:10:11 +0100 |
urbanc |
merged the silly lemmas into the eqvt proof of subtype
|
changeset |
files
|
| Wed, 11 Jan 2006 17:07:57 +0100 |
urbanc |
tuned proofs
|
changeset |
files
|
| Wed, 11 Jan 2006 14:00:11 +0100 |
urbanc |
tuned the eqvt-proof
|
changeset |
files
|
| Wed, 11 Jan 2006 12:21:01 +0100 |
urbanc |
rolled back the last addition since these lemmas were already
|
changeset |
files
|
| Wed, 11 Jan 2006 12:14:25 +0100 |
urbanc |
added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)
|
changeset |
files
|
| Wed, 11 Jan 2006 12:11:53 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Wed, 11 Jan 2006 11:00:26 +0100 |
paulson |
tidied, and added missing thm divide_less_eq_1_neg
|
changeset |
files
|
| Wed, 11 Jan 2006 10:59:55 +0100 |
paulson |
tidied, and giving theorems names
|
changeset |
files
|
| Wed, 11 Jan 2006 03:10:04 +0100 |
huffman |
add transitivity rules
|
changeset |
files
|
| Wed, 11 Jan 2006 00:11:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 11 Jan 2006 00:11:02 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:36:59 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:34:04 +0100 |
wenzelm |
generic attributes;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:42 +0100 |
wenzelm |
* ML: generic context, data, attributes;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:41 +0100 |
wenzelm |
added context_of -- generic context;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:39 +0100 |
wenzelm |
generic attributes;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:38 +0100 |
wenzelm |
print rules: generic context;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:37 +0100 |
wenzelm |
Specification.pretty_consts ctxt;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:36 +0100 |
wenzelm |
generic data and attributes;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:35 +0100 |
wenzelm |
added rule, declaration;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:34 +0100 |
wenzelm |
added generic syntax;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:33 +0100 |
wenzelm |
tuned dependencies;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:32 +0100 |
wenzelm |
added declaration_attribute;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:31 +0100 |
wenzelm |
support for generic contexts with data;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:30 +0100 |
wenzelm |
fix_tac: no warning;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:29 +0100 |
wenzelm |
generic attributes;
|
changeset |
files
|
| Tue, 10 Jan 2006 19:33:27 +0100 |
wenzelm |
Attrib.rule;
|
changeset |
files
|
| Tue, 10 Jan 2006 15:23:31 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Tue, 10 Jan 2006 02:32:10 +0100 |
urbanc |
added the lemmas supp_char and supp_string
|
changeset |
files
|
| Mon, 09 Jan 2006 15:55:15 +0100 |
urbanc |
added some lemmas to the collection "abs_fresh"
|
changeset |
files
|
| Mon, 09 Jan 2006 13:29:08 +0100 |
paulson |
_E suffix for compatibility with AddIffs
|
changeset |
files
|
| Mon, 09 Jan 2006 13:28:34 +0100 |
paulson |
tidied
|
changeset |
files
|
| Mon, 09 Jan 2006 13:28:06 +0100 |
paulson |
simplified the special-case simprules
|
changeset |
files
|
| Mon, 09 Jan 2006 13:27:44 +0100 |
paulson |
theorems need names
|
changeset |
files
|
| Mon, 09 Jan 2006 00:05:10 +0100 |
urbanc |
commented the transitivity and narrowing proof
|
changeset |
files
|
| Sat, 07 Jan 2006 23:28:01 +0100 |
wenzelm |
Theory specifications --- with type-inference, but no internal polymorphism.
|
changeset |
files
|
| Sat, 07 Jan 2006 23:28:00 +0100 |
wenzelm |
added infer_type, declared_type;
|
changeset |
files
|
| Sat, 07 Jan 2006 23:27:59 +0100 |
wenzelm |
added param, spec, named_spec;
|
changeset |
files
|
| Sat, 07 Jan 2006 23:27:58 +0100 |
wenzelm |
added init;
|
changeset |
files
|
| Sat, 07 Jan 2006 23:27:56 +0100 |
wenzelm |
added 'axiomatization';
|
changeset |
files
|
| Sat, 07 Jan 2006 23:27:55 +0100 |
wenzelm |
Specification.pretty_consts;
|
changeset |
files
|
| Sat, 07 Jan 2006 23:27:53 +0100 |
wenzelm |
gen_names: preserve empty names;
|
changeset |
files
|
| Sat, 07 Jan 2006 23:27:52 +0100 |
wenzelm |
added Isar/specification.ML;
|
changeset |
files
|
| Sat, 07 Jan 2006 23:27:51 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Sat, 07 Jan 2006 13:50:38 +0100 |
urbanc |
another change for the new induct-method
|
changeset |
files
|
| Sat, 07 Jan 2006 12:28:25 +0100 |
wenzelm |
RuleCases.make_nested;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:35 +0100 |
wenzelm |
support nested cases;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:33 +0100 |
wenzelm |
support nested cases;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:32 +0100 |
wenzelm |
RuleCases.make_common;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:31 +0100 |
wenzelm |
pretty_locale: backquote notes;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:29 +0100 |
wenzelm |
RuleCases.make_simple;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:28 +0100 |
wenzelm |
tuned order;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:27 +0100 |
wenzelm |
added backquote;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:25 +0100 |
wenzelm |
RuleCases.make_common/nested;
|
changeset |
files
|
| Sat, 07 Jan 2006 12:26:23 +0100 |
wenzelm |
* Provers/induct: improved simultaneous goals -- nested cases;
|
changeset |
files
|
| Sat, 07 Jan 2006 11:43:42 +0100 |
urbanc |
added private datatype nprod (copy of prod) to be
|
changeset |
files
|
| Sat, 07 Jan 2006 11:36:58 +0100 |
urbanc |
changed PRO_RED proof to conform with the new induction rules
|
changeset |
files
|
| Fri, 06 Jan 2006 18:18:16 +0100 |
wenzelm |
prep_meta_eq: reuse mk_rews of local simpset;
|
changeset |
files
|
| Fri, 06 Jan 2006 18:18:15 +0100 |
wenzelm |
removed obsolete eqrule_HOL_data.ML;
|
changeset |
files
|
| Fri, 06 Jan 2006 18:18:14 +0100 |
wenzelm |
removed obsolete eqrule_FOL_data.ML;
|
changeset |
files
|
| Fri, 06 Jan 2006 18:18:13 +0100 |
wenzelm |
simplified EqSubst setup;
|
changeset |
files
|
| Fri, 06 Jan 2006 18:18:12 +0100 |
wenzelm |
obsolete, reuse mk_rews of local simpset;
|
changeset |
files
|
| Fri, 06 Jan 2006 15:18:22 +0100 |
wenzelm |
Toplevel.theory_to_proof;
|
changeset |
files
|
| Fri, 06 Jan 2006 15:18:21 +0100 |
wenzelm |
transactions now always see quasi-functional intermediate checkpoint;
|
changeset |
files
|
| Fri, 06 Jan 2006 15:18:20 +0100 |
wenzelm |
tuned EqSubst setup;
|
changeset |
files
|
| Fri, 06 Jan 2006 15:18:19 +0100 |
wenzelm |
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
|
changeset |
files
|
| Thu, 05 Jan 2006 22:30:00 +0100 |
wenzelm |
hide type datatype node;
|
changeset |
files
|
| Thu, 05 Jan 2006 22:29:59 +0100 |
wenzelm |
tuned print_theorems_theory;
|
changeset |
files
|
| Thu, 05 Jan 2006 22:29:58 +0100 |
wenzelm |
Toplevel.proof_position_of;
|
changeset |
files
|
| Thu, 05 Jan 2006 22:29:57 +0100 |
wenzelm |
store_thm: transfer to current context, i.e. the target theory;
|
changeset |
files
|
| Thu, 05 Jan 2006 22:29:55 +0100 |
wenzelm |
replaced swap by contrapos_np;
|
changeset |
files
|
| Thu, 05 Jan 2006 22:29:53 +0100 |
wenzelm |
added setminus;
|
changeset |
files
|
| Thu, 05 Jan 2006 17:16:40 +0100 |
wenzelm |
proper handling of simultaneous goals and mutual rules;
|
changeset |
files
|
| Thu, 05 Jan 2006 17:16:38 +0100 |
wenzelm |
provide projections of induct_weak, induct_unsafe;
|
changeset |
files
|
| Thu, 05 Jan 2006 17:14:08 +0100 |
wenzelm |
added strict_mutual_rule;
|
changeset |
files
|
| Thu, 05 Jan 2006 17:14:07 +0100 |
wenzelm |
RuleCases.strict_mutual_rule;
|
changeset |
files
|
| Thu, 05 Jan 2006 12:09:26 +0100 |
urbanc |
changed the name of the type "nOption" to "noption".
|
changeset |
files
|
| Wed, 04 Jan 2006 20:20:25 +0100 |
urbanc |
added "fresh_singleton" lemma
|
changeset |
files
|
| Wed, 04 Jan 2006 19:53:39 +0100 |
urbanc |
added more documentation; will now try out a modification
|
changeset |
files
|
| Wed, 04 Jan 2006 19:22:53 +0100 |
nipkow |
Reversed Larry's option/iff change.
|
changeset |
files
|
| Wed, 04 Jan 2006 17:04:11 +0100 |
haftmann |
substantial additions using locales
|
changeset |
files
|
| Wed, 04 Jan 2006 17:03:43 +0100 |
haftmann |
exported read|cert_arity interfaces
|
changeset |
files
|
| Wed, 04 Jan 2006 16:38:40 +0100 |
nipkow |
trace_simp_depth_limit is 1 by default
|
changeset |
files
|
| Wed, 04 Jan 2006 16:37:57 +0100 |
nipkow |
removed pointless trace msg.
|
changeset |
files
|
| Wed, 04 Jan 2006 16:14:15 +0100 |
paulson |
preservation of names
|
changeset |
files
|
| Wed, 04 Jan 2006 16:13:53 +0100 |
paulson |
a few more named lemmas
|
changeset |
files
|
| Wed, 04 Jan 2006 10:28:31 +0100 |
haftmann |
fix: reintroduced pred_ctxt in gen_add_locale
|
changeset |
files
|
| Wed, 04 Jan 2006 01:04:59 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 04 Jan 2006 01:00:52 +0100 |
wenzelm |
* Pure/Isar: Toplevel.theory_theory_to_proof;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:49 +0100 |
wenzelm |
added unlocalize_mfix;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:48 +0100 |
wenzelm |
added unlocalize_mixfix;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:47 +0100 |
wenzelm |
added theory_to_theory_to_proof, which may change theory before entering the proof;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:45 +0100 |
wenzelm |
moved forget_proof to toplevel.ML;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:43 +0100 |
wenzelm |
Toplevel.forget_proof;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:42 +0100 |
wenzelm |
adapted Toplevel.Proof;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:40 +0100 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Wed, 04 Jan 2006 00:52:38 +0100 |
wenzelm |
more stuff;
|
changeset |
files
|
| Tue, 03 Jan 2006 15:44:39 +0100 |
paulson |
Provers/classical: stricter checks to ensure that supplied intro, dest and
|
changeset |
files
|
| Tue, 03 Jan 2006 15:43:54 +0100 |
paulson |
added explicit paths to required theories
|
changeset |
files
|
| Tue, 03 Jan 2006 14:07:17 +0100 |
wenzelm |
added implementation manual;
|
changeset |
files
|
| Tue, 03 Jan 2006 13:59:55 +0100 |
wenzelm |
more stuff;
|
changeset |
files
|
| Tue, 03 Jan 2006 11:57:33 +0100 |
wenzelm |
fixed LaTeX source;
|
changeset |
files
|
| Tue, 03 Jan 2006 11:33:18 +0100 |
haftmann |
class now a keyword
|
changeset |
files
|
| Tue, 03 Jan 2006 11:32:55 +0100 |
haftmann |
class now an keyword, quoted where necessary
|
changeset |
files
|
| Tue, 03 Jan 2006 11:32:16 +0100 |
haftmann |
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
|
changeset |
files
|
| Tue, 03 Jan 2006 11:31:15 +0100 |
haftmann |
rearranged burrow_split to fold_burrow to allow composition with fold_map
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:30 +0100 |
wenzelm |
added unfolding(_i);
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:29 +0100 |
wenzelm |
unparse String/AltString: escape quotes;
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:28 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:26 +0100 |
wenzelm |
avoid hardwired Trueprop;
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:24 +0100 |
wenzelm |
added 'using' command;
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:23 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:22 +0100 |
wenzelm |
added IsarImplementation;
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:20 +0100 |
wenzelm |
updated -- lost update!?
|
changeset |
files
|
| Tue, 03 Jan 2006 00:06:18 +0100 |
wenzelm |
* Pure/Isar: new command 'unfolding';
|
changeset |
files
|
| Mon, 02 Jan 2006 20:50:17 +0100 |
wenzelm |
ISABELLE_USER for remote cvs access;
|
changeset |
files
|
| Mon, 02 Jan 2006 20:42:12 +0100 |
wenzelm |
outline;
|
changeset |
files
|
| Mon, 02 Jan 2006 20:16:52 +0100 |
wenzelm |
"The Isabelle/Isar Implementation" manual;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:44 +0100 |
wenzelm |
* Provers/classical: removed obsolete classical version of elim_format;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:43 +0100 |
wenzelm |
tuned forall_intr_vars;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:42 +0100 |
wenzelm |
added classical_rule, which replaces Data.make_elim;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:41 +0100 |
wenzelm |
explicitly reject consts *Goal*, *False*;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:40 +0100 |
wenzelm |
elim rules: Classical.classical_rule;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:39 +0100 |
wenzelm |
removed obsolete cla_dist_concl;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:38 +0100 |
wenzelm |
removed classical elim_format;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:36 +0100 |
wenzelm |
removed obsolete Provers/make_elim.ML;
|
changeset |
files
|
| Sat, 31 Dec 2005 21:49:35 +0100 |
wenzelm |
obsolete, see classical_rule in Provers/classical.ML;
|
changeset |
files
|
| Sat, 31 Dec 2005 13:03:55 +0100 |
wenzelm |
more robust phantomsection;
|
changeset |
files
|
| Fri, 30 Dec 2005 16:57:00 +0100 |
wenzelm |
require cla_dist_concl, avoid assumptions about concrete syntax;
|
changeset |
files
|
| Fri, 30 Dec 2005 16:56:59 +0100 |
wenzelm |
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
|
changeset |
files
|
| Fri, 30 Dec 2005 16:56:58 +0100 |
wenzelm |
provide equality_name, not_name;
|
changeset |
files
|
| Fri, 30 Dec 2005 16:56:57 +0100 |
wenzelm |
fixed final_consts;
|
changeset |
files
|
| Fri, 30 Dec 2005 16:56:56 +0100 |
wenzelm |
provide cla_dist_concl;
|
changeset |
files
|
| Fri, 30 Dec 2005 16:56:54 +0100 |
wenzelm |
non-PDF: phantomsection;
|
changeset |
files
|
| Thu, 29 Dec 2005 16:10:58 +0100 |
haftmann |
added atom keyword
|
changeset |
files
|
| Thu, 29 Dec 2005 15:31:27 +0100 |
haftmann |
changes in code generator keywords
|
changeset |
files
|
| Thu, 29 Dec 2005 15:31:10 +0100 |
haftmann |
adaptions to changes in code generator
|
changeset |
files
|
| Thu, 29 Dec 2005 15:30:52 +0100 |
haftmann |
slight improvements
|
changeset |
files
|
| Wed, 28 Dec 2005 21:14:23 +0100 |
haftmann |
slightly improved serialization
|
changeset |
files
|
| Tue, 27 Dec 2005 15:24:40 +0100 |
haftmann |
substantial improvements in code generating
|
changeset |
files
|
| Tue, 27 Dec 2005 15:24:23 +0100 |
haftmann |
added map_index
|
changeset |
files
|
| Fri, 23 Dec 2005 20:02:30 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 23 Dec 2005 18:36:27 +0100 |
wenzelm |
removed obsolete atomize_old;
|
changeset |
files
|
| Fri, 23 Dec 2005 18:36:26 +0100 |
wenzelm |
removed obsolete induct_atomize_old;
|
changeset |
files
|
| Fri, 23 Dec 2005 17:37:54 +0100 |
paulson |
the "skolem" attribute and better initialization of the clause database
|
changeset |
files
|
| Fri, 23 Dec 2005 17:36:00 +0100 |
paulson |
blacklist of prolific theorems (must be replaced by an attribute later
|
changeset |
files
|
| Fri, 23 Dec 2005 17:34:46 +0100 |
paulson |
tidied
|
changeset |
files
|
| Fri, 23 Dec 2005 15:21:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:18:13 +0100 |
wenzelm |
* Provers/induct: support simultaneous goals with mutual rules;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:58 +0100 |
wenzelm |
induct etc.: admit multiple rules;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:56 +0100 |
wenzelm |
backpatching of Substring.full;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:55 +0100 |
wenzelm |
goal/qed: proper treatment of two levels of conjunctions;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:53 +0100 |
wenzelm |
Logic.mk_conjunction_list;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:52 +0100 |
wenzelm |
turned bicompose_no_flatten into compose_no_flatten, without elimination;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:49 +0100 |
wenzelm |
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:48 +0100 |
wenzelm |
added mk_conjunction_list2;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:46 +0100 |
wenzelm |
conj_elim_precise: proper treatment of nested conjunctions;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:46 +0100 |
wenzelm |
Thm.compose_no_flatten;
|
changeset |
files
|
| Fri, 23 Dec 2005 15:16:44 +0100 |
wenzelm |
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
|
changeset |
files
|
| Fri, 23 Dec 2005 14:33:28 +0100 |
haftmann |
is_prefix
|
changeset |
files
|
| Thu, 22 Dec 2005 19:08:15 +0100 |
haftmann |
slight improvements
|
changeset |
files
|
| Thu, 22 Dec 2005 17:57:09 +0100 |
nipkow |
more lemmas
|
changeset |
files
|
| Thu, 22 Dec 2005 14:22:11 +0100 |
paulson |
shorter proof
|
changeset |
files
|
| Thu, 22 Dec 2005 13:31:58 +0100 |
berghofe |
Tuned syntax for perm.
|
changeset |
files
|
| Thu, 22 Dec 2005 13:00:53 +0100 |
nipkow |
new lemmas
|
changeset |
files
|
| Thu, 22 Dec 2005 12:27:10 +0100 |
paulson |
Fixed a use of an outdated Substring function
|
changeset |
files
|
| Thu, 22 Dec 2005 00:41:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:22 +0100 |
wenzelm |
exh_casedist2: norm_hhf_eq;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:20 +0100 |
wenzelm |
added bicompose_no_flatten, which refrains from
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:19 +0100 |
wenzelm |
bicompose_proof: no_flatten;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:18 +0100 |
wenzelm |
conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:17 +0100 |
wenzelm |
Transform mutual rule into projection.
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:15 +0100 |
wenzelm |
added Provers/project_rule.ML
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:14 +0100 |
wenzelm |
structure ProjectRule;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:12 +0100 |
wenzelm |
* induct: improved treatment of mutual goals and mutual rules;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:11 +0100 |
wenzelm |
updated auxiliary facts for induct method;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:10 +0100 |
wenzelm |
prop_tr': proper handling of aprop marked as bound;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:09 +0100 |
wenzelm |
consume: expand defs in prems of concls;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:08 +0100 |
wenzelm |
cases: main is_proper flag;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:07 +0100 |
wenzelm |
auto cases: marked improper;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:06 +0100 |
wenzelm |
conjunction_tac: single goal;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:04 +0100 |
wenzelm |
CONJUNCTS2;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:03 +0100 |
wenzelm |
rule_context: numbered cases;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:01 +0100 |
wenzelm |
conjunction_tac: single goal;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:29:00 +0100 |
wenzelm |
renamed imp_cong' to imp_cong_rule;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:58 +0100 |
wenzelm |
mk_conjunction: proper treatment of bounds;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:54 +0100 |
wenzelm |
fixed has_internal;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:53 +0100 |
wenzelm |
Tactic.precise_conjunction_tac;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:52 +0100 |
wenzelm |
added locale meta_conjunction_syntax and various conjunction rules;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:51 +0100 |
wenzelm |
simplified setup: removed dest_concls, local_impI, conjI;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:49 +0100 |
wenzelm |
induct_rulify;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:47 +0100 |
wenzelm |
actually produce projected rules;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:46 +0100 |
wenzelm |
*.inducts holds all projected rules;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:44 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:43 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:41 +0100 |
wenzelm |
mutual induct with *.inducts;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:39 +0100 |
wenzelm |
wf_induct_rule: consumes 1;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:36 +0100 |
wenzelm |
structure ProjectRule;
|
changeset |
files
|
| Thu, 22 Dec 2005 00:28:34 +0100 |
wenzelm |
updated auxiliary facts for induct method;
|
changeset |
files
|
| Wed, 21 Dec 2005 17:00:57 +0100 |
haftmann |
slight improvements
|
changeset |
files
|
| Wed, 21 Dec 2005 15:19:16 +0100 |
haftmann |
slight improvements in name handling
|
changeset |
files
|
| Wed, 21 Dec 2005 15:18:57 +0100 |
haftmann |
slight refinements
|
changeset |
files
|
| Wed, 21 Dec 2005 15:18:36 +0100 |
haftmann |
added eq_ord
|
changeset |
files
|
| Wed, 21 Dec 2005 15:18:17 +0100 |
haftmann |
slight clean ups
|
changeset |
files
|
| Wed, 21 Dec 2005 13:25:20 +0100 |
haftmann |
discontinued unflat in favour of burrow and burrow_split
|
changeset |
files
|
| Wed, 21 Dec 2005 12:06:08 +0100 |
paulson |
new hash table module in HOL/Too/s
|
changeset |
files
|
| Wed, 21 Dec 2005 12:05:47 +0100 |
paulson |
modified suffix for [iff] attribute
|
changeset |
files
|
| Wed, 21 Dec 2005 12:02:57 +0100 |
paulson |
removed or modified some instances of [iff]
|
changeset |
files
|
| Tue, 20 Dec 2005 22:06:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Dec 2005 09:02:41 +0100 |
haftmann |
added .cvsignore
|
changeset |
files
|
| Tue, 20 Dec 2005 09:01:48 +0100 |
haftmann |
removed improper .cvsignore
|
changeset |
files
|
| Tue, 20 Dec 2005 08:58:36 +0100 |
haftmann |
removed superfluos is_prefix functions
|
changeset |
files
|
| Tue, 20 Dec 2005 08:38:43 +0100 |
haftmann |
resolved shadowing of Library.find_first
|
changeset |
files
|
| Tue, 20 Dec 2005 08:38:10 +0100 |
haftmann |
removed infix prefix, introduces burrow
|
changeset |
files
|
| Tue, 20 Dec 2005 04:29:25 +0100 |
mengj |
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
|
changeset |
files
|
| Tue, 20 Dec 2005 04:27:46 +0100 |
mengj |
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
|
changeset |
files
|
| Mon, 19 Dec 2005 16:07:19 +0100 |
urbanc |
made the changes according to Florian's re-arranging of
|
changeset |
files
|
| Mon, 19 Dec 2005 15:29:51 +0100 |
urbanc |
added proofs to show that every atom-kind combination
|
changeset |
files
|
| Mon, 19 Dec 2005 12:58:15 +0100 |
urbanc |
added thms to perm_compose (so far only composition
|
changeset |
files
|
| Mon, 19 Dec 2005 12:09:56 +0100 |
urbanc |
tuned one comment
|
changeset |
files
|
| Mon, 19 Dec 2005 12:08:16 +0100 |
urbanc |
fixed a bug that occured when more than one atom-type
|
changeset |
files
|
| Mon, 19 Dec 2005 09:19:08 +0100 |
nipkow |
fixed proof
|
changeset |
files
|
| Sun, 18 Dec 2005 20:10:15 +0100 |
urbanc |
more cleaning up - this time of the cp-instance
|
changeset |
files
|
| Sun, 18 Dec 2005 14:36:42 +0100 |
urbanc |
improved the finite-support proof
|
changeset |
files
|
| Sun, 18 Dec 2005 13:38:06 +0100 |
urbanc |
improved the code for showing that a type is
|
changeset |
files
|
| Sat, 17 Dec 2005 01:58:41 +0100 |
wenzelm |
simp del: empty_Collect_eq;
|
changeset |
files
|
| Sat, 17 Dec 2005 01:00:40 +0100 |
wenzelm |
sort_distinct;
|
changeset |
files
|
| Sat, 17 Dec 2005 01:00:38 +0100 |
wenzelm |
added sort_distinct;
|
changeset |
files
|
| Fri, 16 Dec 2005 18:22:58 +0100 |
urbanc |
added container-lemma fresh_eqvt
|
changeset |
files
|
| Fri, 16 Dec 2005 18:20:59 +0100 |
urbanc |
I think the earlier version was completely broken
|
changeset |
files
|
| Fri, 16 Dec 2005 18:20:03 +0100 |
urbanc |
tuned more proofs
|
changeset |
files
|
| Fri, 16 Dec 2005 16:59:32 +0100 |
nipkow |
new lemmas
|
changeset |
files
|
| Fri, 16 Dec 2005 16:00:58 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
changeset |
files
|
| Fri, 16 Dec 2005 15:52:05 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
changeset |
files
|
| Fri, 16 Dec 2005 12:15:54 +0100 |
paulson |
hashing to eliminate the output of duplicate clauses
|
changeset |
files
|
| Fri, 16 Dec 2005 11:51:24 +0100 |
paulson |
hash tables from SML/NJ
|
changeset |
files
|
| Fri, 16 Dec 2005 09:00:11 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
changeset |
files
|
| Thu, 15 Dec 2005 21:51:31 +0100 |
urbanc |
there was a small error in the last commit - fixed now
|
changeset |
files
|
| Thu, 15 Dec 2005 21:49:14 +0100 |
urbanc |
tuned more proof and added in-file documentation
|
changeset |
files
|
| Thu, 15 Dec 2005 19:42:03 +0100 |
wenzelm |
improved proofs;
|
changeset |
files
|
| Thu, 15 Dec 2005 19:42:02 +0100 |
wenzelm |
acc_induct: proper tags;
|
changeset |
files
|
| Thu, 15 Dec 2005 19:42:00 +0100 |
wenzelm |
removed obsolete/unused setup_induction;
|
changeset |
files
|
| Thu, 15 Dec 2005 18:13:40 +0100 |
urbanc |
tuned the proof of transitivity/narrowing
|
changeset |
files
|
| Thu, 15 Dec 2005 15:26:37 +0100 |
paulson |
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
|
changeset |
files
|
| Thu, 15 Dec 2005 11:53:38 +0100 |
urbanc |
made further tunings
|
changeset |
files
|
| Thu, 15 Dec 2005 05:47:26 +0100 |
mengj |
Added functions to test equivalence between clauses.
|
changeset |
files
|
| Wed, 14 Dec 2005 22:05:22 +0100 |
webertj |
ex/Sudoku.thy
|
changeset |
files
|
| Wed, 14 Dec 2005 18:01:50 +0100 |
paulson |
deleted redundant (looping!) simprule
|
changeset |
files
|
| Wed, 14 Dec 2005 16:14:41 +0100 |
paulson |
modified example for new clauses
|
changeset |
files
|
| Wed, 14 Dec 2005 16:14:26 +0100 |
paulson |
removal of some redundancies (e.g. one-point-rules) in clause production
|
changeset |
files
|
| Wed, 14 Dec 2005 16:13:09 +0100 |
paulson |
removed unused function repeat_RS
|
changeset |
files
|
| Wed, 14 Dec 2005 06:19:33 +0100 |
mengj |
Changed literals' ordering and the functions for sorting literals.
|
changeset |
files
|
| Wed, 14 Dec 2005 01:40:43 +0100 |
mengj |
1. changed fol_type, it's not a string type anymore.
|
changeset |
files
|
| Wed, 14 Dec 2005 01:39:41 +0100 |
mengj |
changed ATP input files' names and location.
|
changeset |
files
|
| Tue, 13 Dec 2005 19:32:36 +0100 |
wenzelm |
Potentially infinite lists as greatest fixed-point.
|
changeset |
files
|
| Tue, 13 Dec 2005 19:32:06 +0100 |
wenzelm |
Provers/induct: coinduct;
|
changeset |
files
|
| Tue, 13 Dec 2005 19:32:05 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 13 Dec 2005 19:32:04 +0100 |
wenzelm |
added HOL/Library/Coinductive_List.thy;
|
changeset |
files
|
| Tue, 13 Dec 2005 18:11:21 +0100 |
urbanc |
added a fresh_left lemma that contains all instantiation
|
changeset |
files
|
| Tue, 13 Dec 2005 16:30:50 +0100 |
urbanc |
initial commit (not to be seen by the public)
|
changeset |
files
|
| Tue, 13 Dec 2005 16:25:10 +0100 |
chaieb |
simpset for computation in raw_arith_tac added just as comment, nothing changed!
|
changeset |
files
|
| Tue, 13 Dec 2005 16:24:12 +0100 |
chaieb |
deals with Suc in mod expressions
|
changeset |
files
|
| Tue, 13 Dec 2005 15:46:41 +0100 |
wenzelm |
Poplog/pml provides a proper print function already!
|
changeset |
files
|
| Tue, 13 Dec 2005 15:34:21 +0100 |
paulson |
meson no longer does these examples
|
changeset |
files
|
| Tue, 13 Dec 2005 15:34:02 +0100 |
paulson |
now generates the name "append"
|
changeset |
files
|
| Tue, 13 Dec 2005 15:27:43 +0100 |
paulson |
removal of functional reflexivity axioms
|
changeset |
files
|
| Tue, 13 Dec 2005 10:39:32 +0100 |
berghofe |
list_of_indset now also generates code for set type.
|
changeset |
files
|
| Mon, 12 Dec 2005 17:24:06 +0100 |
haftmann |
added generic name mangler
|
changeset |
files
|
| Mon, 12 Dec 2005 15:37:35 +0100 |
haftmann |
improvement in eq handling
|
changeset |
files
|
| Mon, 12 Dec 2005 15:37:05 +0100 |
haftmann |
improvements in class and eq handling
|
changeset |
files
|
| Mon, 12 Dec 2005 15:36:46 +0100 |
haftmann |
added dummy 'print' to non-polyml systems
|
changeset |
files
|
| Sun, 11 Dec 2005 11:57:01 +0100 |
urbanc |
ISAR-fied some proofs
|
changeset |
files
|
| Sun, 11 Dec 2005 01:21:26 +0100 |
urbanc |
completed the sn proof and changed the manual
|
changeset |
files
|
| Sat, 10 Dec 2005 00:11:35 +0100 |
urbanc |
changed the types in accordance with Florian's changes
|
changeset |
files
|
| Fri, 09 Dec 2005 15:25:52 +0100 |
haftmann |
substantial improvements for class code generation
|
changeset |
files
|
| Fri, 09 Dec 2005 15:25:29 +0100 |
haftmann |
improved extraction interface
|
changeset |
files
|
| Fri, 09 Dec 2005 12:38:49 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Fri, 09 Dec 2005 09:06:45 +0100 |
haftmann |
oriented result pairs in PureThy
|
changeset |
files
|
| Thu, 08 Dec 2005 20:16:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 08 Dec 2005 20:16:10 +0100 |
wenzelm |
removed Syntax.deskolem;
|
changeset |
files
|
| Thu, 08 Dec 2005 20:16:04 +0100 |
wenzelm |
swap: no longer pervasive;
|
changeset |
files
|
| Thu, 08 Dec 2005 20:15:57 +0100 |
wenzelm |
replaced swap by contrapos_np;
|
changeset |
files
|
| Thu, 08 Dec 2005 20:15:50 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 08 Dec 2005 20:15:41 +0100 |
wenzelm |
Cla.swap;
|
changeset |
files
|
| Thu, 08 Dec 2005 20:15:34 +0100 |
wenzelm |
removed hint for Classical.swap, which is not really user-level anyway;
|
changeset |
files
|
| Thu, 08 Dec 2005 12:50:04 +0100 |
wenzelm |
tuned sources and proofs
|
changeset |
files
|
| Thu, 08 Dec 2005 12:50:03 +0100 |
wenzelm |
Classical.swap;
|
changeset |
files
|
| Thu, 08 Dec 2005 12:50:02 +0100 |
wenzelm |
* HOL: Theorem 'swap' is no longer bound at the ML top-level.
|
changeset |
files
|
| Thu, 08 Dec 2005 10:17:21 +0100 |
berghofe |
Adapted to new type of PureThy.add_defs_i.
|
changeset |
files
|
| Wed, 07 Dec 2005 16:47:04 +0100 |
wenzelm |
replaced swap by Classical.swap;
|
changeset |
files
|
| Wed, 07 Dec 2005 15:23:22 +0100 |
wenzelm |
avoid unportable tail;
|
changeset |
files
|
| Wed, 07 Dec 2005 12:33:38 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Tue, 06 Dec 2005 17:26:26 +0100 |
haftmann |
removed thms 'swap' and 'nth_map' from ML toplevel
|
changeset |
files
|
| Tue, 06 Dec 2005 17:11:40 +0100 |
haftmann |
improved serialization of classes to haskell
|
changeset |
files
|
| Tue, 06 Dec 2005 16:07:25 +0100 |
haftmann |
improved class handling
|
changeset |
files
|
| Tue, 06 Dec 2005 16:07:10 +0100 |
haftmann |
added 'dig' combinator
|
changeset |
files
|
| Tue, 06 Dec 2005 09:04:09 +0100 |
haftmann |
re-oriented some result tuples in PureThy
|
changeset |
files
|
| Tue, 06 Dec 2005 06:22:14 +0100 |
mengj |
Added more functions for new type embedding of HOL clauses.
|
changeset |
files
|
| Tue, 06 Dec 2005 06:21:07 +0100 |
mengj |
Added new type embedding methods for translating HOL clauses.
|
changeset |
files
|
| Mon, 05 Dec 2005 18:19:49 +0100 |
urbanc |
added code to say that discrete types (nat, bool, char)
|
changeset |
files
|
| Mon, 05 Dec 2005 17:02:20 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Mon, 05 Dec 2005 15:55:19 +0100 |
urbanc |
transitivity should be now in a reasonable state. But
|
changeset |
files
|
| Mon, 05 Dec 2005 10:33:30 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Mon, 05 Dec 2005 10:32:37 +0100 |
urbanc |
ISAR-fied two proofs
|
changeset |
files
|
| Mon, 05 Dec 2005 00:39:18 +0100 |
berghofe |
Adapted to new type of store_thmss(_atts).
|
changeset |
files
|
| Mon, 05 Dec 2005 00:38:07 +0100 |
berghofe |
Added store_thmss_atts to signature again.
|
changeset |
files
|
| Sun, 04 Dec 2005 12:40:39 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Sun, 04 Dec 2005 12:25:57 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Sun, 04 Dec 2005 12:14:40 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Sun, 04 Dec 2005 12:14:27 +0100 |
urbanc |
added an Isar-proof for the abs_ALL lemma
|
changeset |
files
|
| Sun, 04 Dec 2005 12:14:03 +0100 |
urbanc |
tuning
|
changeset |
files
|
| Fri, 02 Dec 2005 22:57:36 +0100 |
wenzelm |
defines: beta/eta contract lhs;
|
changeset |
files
|
| Fri, 02 Dec 2005 22:54:52 +0100 |
wenzelm |
asts_to_terms: builtin free_fixed translation makes local binders work properly;
|
changeset |
files
|
| Fri, 02 Dec 2005 22:54:51 +0100 |
wenzelm |
mixfix_args: 1 for binders;
|
changeset |
files
|
| Fri, 02 Dec 2005 22:54:50 +0100 |
wenzelm |
removed fixed_tr: now handled in syntax module;
|
changeset |
files
|
| Fri, 02 Dec 2005 22:54:48 +0100 |
wenzelm |
added mixfixT;
|
changeset |
files
|
| Fri, 02 Dec 2005 22:54:47 +0100 |
wenzelm |
defs: beta/eta contract lhs;
|
changeset |
files
|
| Fri, 02 Dec 2005 22:54:45 +0100 |
wenzelm |
abs_def: beta/eta contract lhs;
|
changeset |
files
|
| Fri, 02 Dec 2005 16:43:42 +0100 |
krauss |
Added recdef congruence rules for bounded quantifiers and commonly used
|
changeset |
files
|
| Fri, 02 Dec 2005 16:05:31 +0100 |
haftmann |
various improvements
|
changeset |
files
|
| Fri, 02 Dec 2005 16:05:12 +0100 |
haftmann |
adjusted to improved code generator interface
|
changeset |
files
|
| Fri, 02 Dec 2005 16:04:48 +0100 |
haftmann |
added perhaps option combinator
|
changeset |
files
|
| Fri, 02 Dec 2005 16:04:29 +0100 |
haftmann |
adopted keyword for code generator
|
changeset |
files
|
| Fri, 02 Dec 2005 13:10:12 +0100 |
berghofe |
Factored out proof for normalization of applications (norm_list).
|
changeset |
files
|
| Fri, 02 Dec 2005 08:06:59 +0100 |
haftmann |
introduced new map2, fold
|
changeset |
files
|
| Thu, 01 Dec 2005 22:43:15 +0100 |
kleing |
typo
|
changeset |
files
|
| Thu, 01 Dec 2005 22:04:27 +0100 |
wenzelm |
simprocs: static evaluation of simpset;
|
changeset |
files
|
| Thu, 01 Dec 2005 22:03:06 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Dec 2005 22:03:05 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Thu, 01 Dec 2005 22:03:04 +0100 |
wenzelm |
ProofContext.lthms_containing: suppress obvious duplicates;
|
changeset |
files
|
| Thu, 01 Dec 2005 22:03:01 +0100 |
wenzelm |
unfold_tac: static evaluation of simpset;
|
changeset |
files
|
| Thu, 01 Dec 2005 18:45:24 +0100 |
wenzelm |
superceded by timestart|stop.bash;
|
changeset |
files
|
| Thu, 01 Dec 2005 18:44:47 +0100 |
wenzelm |
cpu time = user + system;
|
changeset |
files
|
| Thu, 01 Dec 2005 18:41:46 +0100 |
wenzelm |
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
|
changeset |
files
|
| Thu, 01 Dec 2005 18:41:44 +0100 |
berghofe |
assoc_consts and assoc_types now check number of arguments in template.
|
changeset |
files
|
| Thu, 01 Dec 2005 18:39:08 +0100 |
berghofe |
Added new component "sorts" to record datatype_info.
|
changeset |
files
|
| Thu, 01 Dec 2005 18:37:39 +0100 |
wenzelm |
timestop - report timing based on environment (cf. timestart.bash);
|
changeset |
files
|
| Thu, 01 Dec 2005 18:37:22 +0100 |
wenzelm |
timestart - setup bash environment for timing;
|
changeset |
files
|
| Thu, 01 Dec 2005 17:07:50 +0100 |
berghofe |
Improved norm_proof to handle proofs containing term (type) variables
|
changeset |
files
|
| Thu, 01 Dec 2005 15:45:54 +0100 |
paulson |
restoring the old status of subset_refl
|
changeset |
files
|
| Thu, 01 Dec 2005 08:28:02 +0100 |
haftmann |
oriented pairs theory * 'a to 'a * theory
|
changeset |
files
|
| Thu, 01 Dec 2005 06:28:41 +0100 |
urbanc |
initial cleanup to use the new induction method
|
changeset |
files
|
| Thu, 01 Dec 2005 05:20:13 +0100 |
urbanc |
cleaned up further the proofs (diamond still needs work);
|
changeset |
files
|
| Thu, 01 Dec 2005 04:46:17 +0100 |
urbanc |
changed "fresh:" to "avoiding:" and cleaned up the weakening example
|
changeset |
files
|
| Wed, 30 Nov 2005 22:52:50 +0100 |
wenzelm |
match_bind(_i): return terms;
|
changeset |
files
|
| Wed, 30 Nov 2005 22:52:49 +0100 |
wenzelm |
method 'fact': SIMPLE_METHOD, i.e. insert facts;
|
changeset |
files
|
| Wed, 30 Nov 2005 22:52:46 +0100 |
wenzelm |
simulaneous 'def';
|
changeset |
files
|
| Wed, 30 Nov 2005 21:51:23 +0100 |
urbanc |
added facilities to prove the pt and fs instances
|
changeset |
files
|
| Wed, 30 Nov 2005 19:08:51 +0100 |
urbanc |
started to change the transitivity/narrowing case:
|
changeset |
files
|
| Wed, 30 Nov 2005 18:37:12 +0100 |
urbanc |
changed everything until the interesting transitivity_narrowing
|
changeset |
files
|
| Wed, 30 Nov 2005 18:13:31 +0100 |
haftmann |
minor improvements
|
changeset |
files
|
| Wed, 30 Nov 2005 17:56:08 +0100 |
urbanc |
modified almost everything for the new nominal_induct
|
changeset |
files
|
| Wed, 30 Nov 2005 16:59:19 +0100 |
berghofe |
Changed order of predicate arguments and quantifiers in strong induction rule.
|
changeset |
files
|
| Wed, 30 Nov 2005 15:30:08 +0100 |
urbanc |
fixed the lemma where the new names generated by nominal_induct
|
changeset |
files
|
| Wed, 30 Nov 2005 15:27:30 +0100 |
urbanc |
added one clause for substitution in the lambda-case and
|
changeset |
files
|
| Wed, 30 Nov 2005 15:24:32 +0100 |
wenzelm |
added rename_params_rule: recover orginal fresh names in subgoals/cases;
|
changeset |
files
|
| Wed, 30 Nov 2005 15:03:15 +0100 |
urbanc |
changed induction principle and everything to conform with the
|
changeset |
files
|
| Wed, 30 Nov 2005 14:27:50 +0100 |
wenzelm |
fresh: frees instead of terms, rename corresponding params in rule;
|
changeset |
files
|
| Wed, 30 Nov 2005 14:27:09 +0100 |
urbanc |
adapted to the new nominal_induction
|
changeset |
files
|
| Wed, 30 Nov 2005 12:28:47 +0100 |
urbanc |
changed \<sim> of permutation equality to \<triangleq>
|
changeset |
files
|
| Wed, 30 Nov 2005 12:23:35 +0100 |
wenzelm |
fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
|
changeset |
files
|
| Wed, 30 Nov 2005 01:01:15 +0100 |
huffman |
reimplement Case expression pattern matching to support lazy patterns
|
changeset |
files
|
| Wed, 30 Nov 2005 00:59:04 +0100 |
huffman |
add definitions as defs, not axioms
|
changeset |
files
|
| Wed, 30 Nov 2005 00:56:01 +0100 |
huffman |
changed section names
|
changeset |
files
|
| Wed, 30 Nov 2005 00:55:24 +0100 |
huffman |
add xsymbol syntax for u type constructor
|
changeset |
files
|
| Wed, 30 Nov 2005 00:53:30 +0100 |
huffman |
add constant unit_when
|
changeset |
files
|
| Wed, 30 Nov 2005 00:46:08 +0100 |
wenzelm |
proper treatment of tuple/tuple_fun -- nest to the left!
|
changeset |
files
|
| Tue, 29 Nov 2005 23:00:20 +0100 |
wenzelm |
moved nth_list to Pure/library.ML;
|
changeset |
files
|
| Tue, 29 Nov 2005 23:00:03 +0100 |
wenzelm |
added nth_list;
|
changeset |
files
|
| Tue, 29 Nov 2005 22:52:19 +0100 |
wenzelm |
added mk_split;
|
changeset |
files
|
| Tue, 29 Nov 2005 19:26:38 +0100 |
urbanc |
changed the order of the induction variable and the context
|
changeset |
files
|
| Tue, 29 Nov 2005 18:09:12 +0100 |
wenzelm |
reworked version with proper support for defs, fixes, fresh specification;
|
changeset |
files
|
| Tue, 29 Nov 2005 16:05:10 +0100 |
haftmann |
added haskell serializer
|
changeset |
files
|
| Tue, 29 Nov 2005 16:04:57 +0100 |
haftmann |
exported customized syntax interface
|
changeset |
files
|
| Tue, 29 Nov 2005 12:26:22 +0100 |
berghofe |
Corrected atom class constraints in strong induction rule.
|
changeset |
files
|
| Tue, 29 Nov 2005 01:37:01 +0100 |
urbanc |
made some of the theorem look-ups static (by using
|
changeset |
files
|
| Mon, 28 Nov 2005 13:43:56 +0100 |
haftmann |
added (curried) fold2
|
changeset |
files
|
| Mon, 28 Nov 2005 10:58:40 +0100 |
wenzelm |
added proof of measure_induct_rule;
|
changeset |
files
|
| Mon, 28 Nov 2005 07:17:07 +0100 |
mengj |
Added flags for setting and detecting whether a problem needs combinators.
|
changeset |
files
|
| Mon, 28 Nov 2005 07:16:16 +0100 |
mengj |
Only output types if !keep_types is true.
|
changeset |
files
|
| Mon, 28 Nov 2005 07:15:38 +0100 |
mengj |
Added two functions for CNF translation, used by other files.
|
changeset |
files
|
| Mon, 28 Nov 2005 07:15:13 +0100 |
mengj |
Added in four control flags for HOL and FOL translations.
|
changeset |
files
|
| Mon, 28 Nov 2005 07:14:12 +0100 |
mengj |
Slight modification to trace information.
|
changeset |
files
|
| Mon, 28 Nov 2005 07:13:43 +0100 |
mengj |
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
|
changeset |
files
|
| Mon, 28 Nov 2005 07:12:01 +0100 |
mengj |
Only output arities and class relations if !ResClause.keep_types is true.
|
changeset |
files
|
| Mon, 28 Nov 2005 05:03:00 +0100 |
urbanc |
some small tuning
|
changeset |
files
|
| Mon, 28 Nov 2005 00:25:43 +0100 |
urbanc |
ISAR-fied two proofs about equality for abstraction functions.
|
changeset |
files
|
| Sun, 27 Nov 2005 20:06:24 +0100 |
wenzelm |
* Provers/induct: obtain pattern;
|
changeset |
files
|
| Sun, 27 Nov 2005 06:01:11 +0100 |
urbanc |
added an authors section (please let me know if somebody is left out or unhappy)
|
changeset |
files
|
| Sun, 27 Nov 2005 05:09:43 +0100 |
urbanc |
some minor tunings
|
changeset |
files
|
| Sun, 27 Nov 2005 05:00:43 +0100 |
urbanc |
added the version of nominal.thy that contains
|
changeset |
files
|
| Sun, 27 Nov 2005 04:59:20 +0100 |
urbanc |
cleaned up all examples so that they work with the
|
changeset |
files
|
| Sun, 27 Nov 2005 03:55:16 +0100 |
urbanc |
finished cleaning up the parts that collect
|
changeset |
files
|
| Sat, 26 Nov 2005 18:41:41 +0100 |
berghofe |
Corrected treatment of non-recursive abstraction types.
|
changeset |
files
|
| Fri, 25 Nov 2005 21:14:34 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Fri, 25 Nov 2005 20:57:51 +0100 |
wenzelm |
induct: insert defs in object-logic form;
|
changeset |
files
|
| Fri, 25 Nov 2005 19:20:56 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Fri, 25 Nov 2005 19:09:44 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:43 +0100 |
wenzelm |
consume: unfold defs in all major prems;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:42 +0100 |
wenzelm |
revert_skolem: fall back on Syntax.deskolem;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:41 +0100 |
wenzelm |
forall_conv ~1;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:40 +0100 |
wenzelm |
added dummy_pattern;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:38 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:37 +0100 |
wenzelm |
forall_conv: limit prefix;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:36 +0100 |
wenzelm |
fix_tac: proper treatment of major premises in goal;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:35 +0100 |
wenzelm |
removed obsolete dummy paragraphs;
|
changeset |
files
|
| Fri, 25 Nov 2005 18:58:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 25 Nov 2005 17:41:52 +0100 |
haftmann |
code generator: case expressions, improved name resolving
|
changeset |
files
|
| Fri, 25 Nov 2005 14:51:39 +0100 |
urbanc |
added fsub.thy (poplmark challenge) to the examples
|
changeset |
files
|
| Fri, 25 Nov 2005 14:00:22 +0100 |
berghofe |
Fixed problem with strong induction theorem for datatypes containing
|
changeset |
files
|
| Fri, 25 Nov 2005 11:34:37 +0100 |
kleing |
send more information with test-takes-too-long message
|
changeset |
files
|
| Thu, 24 Nov 2005 12:14:56 +0100 |
wenzelm |
fixed spelling of 'case_conclusion';
|
changeset |
files
|
| Thu, 24 Nov 2005 00:00:20 +0100 |
wenzelm |
tuned induct proofs;
|
changeset |
files
|
| Wed, 23 Nov 2005 22:26:13 +0100 |
wenzelm |
tuned induction proofs;
|
changeset |
files
|
| Wed, 23 Nov 2005 22:23:52 +0100 |
wenzelm |
more robust revert_skolem;
|
changeset |
files
|
| Wed, 23 Nov 2005 20:29:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:05 +0100 |
wenzelm |
Provers/induct: definitional insts and fixing;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:04 +0100 |
wenzelm |
consume: proper treatment of defs;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:03 +0100 |
wenzelm |
added case_conclusion attribute;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:02 +0100 |
wenzelm |
(co)induct: taking;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:01 +0100 |
wenzelm |
RuleCases.case_conclusion;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:52:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 23 Nov 2005 18:51:59 +0100 |
wenzelm |
added case_conclusion attribute;
|
changeset |
files
|
| Wed, 23 Nov 2005 17:16:42 +0100 |
haftmann |
improved failure tracking
|
changeset |
files
|
| Tue, 22 Nov 2005 19:37:36 +0100 |
wenzelm |
Datatype_Universe: hide base names only;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:50 +0100 |
wenzelm |
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:48 +0100 |
wenzelm |
cases_tactic;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:47 +0100 |
wenzelm |
moved multi_resolve(s) to drule.ML;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:46 +0100 |
wenzelm |
find_xxxS: term instead of thm;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:44 +0100 |
wenzelm |
export map_tags;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:43 +0100 |
wenzelm |
make coinduct actually work;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:41 +0100 |
wenzelm |
Drule.multi_resolves;
|
changeset |
files
|
| Tue, 22 Nov 2005 19:34:40 +0100 |
wenzelm |
declare coinduct rule;
|
changeset |
files
|
| Tue, 22 Nov 2005 14:32:01 +0100 |
haftmann |
added code generator syntax
|
changeset |
files
|
| Tue, 22 Nov 2005 12:59:25 +0100 |
haftmann |
added codegenerator
|
changeset |
files
|
| Tue, 22 Nov 2005 12:42:59 +0100 |
haftmann |
added code generator syntax
|
changeset |
files
|
| Tue, 22 Nov 2005 10:09:11 +0100 |
paulson |
new treatment of polymorphic types, using Sign.const_typargs
|
changeset |
files
|
| Mon, 21 Nov 2005 16:51:57 +0100 |
haftmann |
added codegen package
|
changeset |
files
|
| Mon, 21 Nov 2005 15:15:32 +0100 |
haftmann |
added serializer
|
changeset |
files
|
| Mon, 21 Nov 2005 11:14:11 +0100 |
paulson |
tweak
|
changeset |
files
|
| Mon, 21 Nov 2005 10:44:14 +0100 |
haftmann |
fixed some inconveniencies in website
|
changeset |
files
|
| Sat, 19 Nov 2005 14:22:28 +0100 |
wenzelm |
CONJUNCTS;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:09 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:08 +0100 |
wenzelm |
Goal.norm_hhf_protected;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:07 +0100 |
wenzelm |
added coinduct attribute;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:06 +0100 |
wenzelm |
added CONJUNCTS: treat conjunction as separate sub-goals;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:05 +0100 |
wenzelm |
simpset: added reorient field, set_reorient;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:04 +0100 |
wenzelm |
tuned norm_hhf_protected;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:03 +0100 |
wenzelm |
removed conj_mono;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:02 +0100 |
wenzelm |
induct: CONJUNCTS for multiple goals;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:01 +0100 |
wenzelm |
tuned induct syntax;
|
changeset |
files
|
| Sat, 19 Nov 2005 14:21:00 +0100 |
wenzelm |
FOL: -p 2;
|
changeset |
files
|
| Fri, 18 Nov 2005 07:13:58 +0100 |
chaieb |
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
|
changeset |
files
|
| Fri, 18 Nov 2005 07:10:37 +0100 |
mengj |
-- changed the interface of functions vampire_oracle and eprover_oracle.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:10:00 +0100 |
mengj |
-- terms are fully typed.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:08:54 +0100 |
mengj |
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:08:18 +0100 |
mengj |
-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:07:47 +0100 |
mengj |
-- added combinator reduction axioms (typed and untyped) for HOL goals.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:07:06 +0100 |
mengj |
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
|
changeset |
files
|
| Fri, 18 Nov 2005 07:06:07 +0100 |
mengj |
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:05:11 +0100 |
mengj |
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
|
changeset |
files
|
| Wed, 16 Nov 2005 19:34:19 +0100 |
wenzelm |
tuned document;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:50:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:49:16 +0100 |
wenzelm |
improved induction proof: local defs/fixes;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:36 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:35 +0100 |
wenzelm |
added deskolem;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:34 +0100 |
wenzelm |
added THEN_ALL_NEW_CASES;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:33 +0100 |
wenzelm |
added revert_skolem, mk_def, add_def;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:32 +0100 |
wenzelm |
ProofContext.mk_def;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:31 +0100 |
wenzelm |
Term.betapplys;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:30 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:29 +0100 |
wenzelm |
added betapplys;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:28 +0100 |
wenzelm |
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:26 +0100 |
wenzelm |
norm_hhf: no normalization of protected props;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:25 +0100 |
wenzelm |
added protect_cong, cong_mono_thm;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:24 +0100 |
wenzelm |
induct: support local definitions to be passed through the induction;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:23 +0100 |
wenzelm |
Trueprop: use ObjectLogic.judgment etc.;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:22 +0100 |
wenzelm |
Term.betapply;
|
changeset |
files
|
| Wed, 16 Nov 2005 15:29:23 +0100 |
paulson |
new version of "tryres" allowing multiple unifiers (apparently needed for
|
changeset |
files
|
| Wed, 16 Nov 2005 14:05:41 +0100 |
wenzelm |
pgmlsymbolson: append Symbol.xsymbolsN at end!
|
changeset |
files
|
| Tue, 15 Nov 2005 14:08:32 +0100 |
wenzelm |
better no -d option;
|
changeset |
files
|
| Tue, 15 Nov 2005 10:11:52 +0100 |
haftmann |
added generic transformators
|
changeset |
files
|
| Mon, 14 Nov 2005 18:25:34 +0100 |
paulson |
removal of is_hol
|
changeset |
files
|
| Mon, 14 Nov 2005 16:26:40 +0100 |
haftmann |
added module system
|
changeset |
files
|
| Mon, 14 Nov 2005 15:23:33 +0100 |
haftmann |
added modules for code generator generation two, not operational yet
|
changeset |
files
|
| Mon, 14 Nov 2005 15:15:34 +0100 |
haftmann |
class_package - operational view on type classes
|
changeset |
files
|
| Mon, 14 Nov 2005 15:15:07 +0100 |
haftmann |
string_of_alist - convenient q'n'd printout function
|
changeset |
files
|
| Mon, 14 Nov 2005 15:14:59 +0100 |
wenzelm |
support for polyml-4.2.0;
|
changeset |
files
|
| Mon, 14 Nov 2005 15:14:32 +0100 |
haftmann |
new syntax for class_package
|
changeset |
files
|
| Mon, 14 Nov 2005 14:37:48 +0100 |
wenzelm |
added const_instance;
|
changeset |
files
|
| Mon, 14 Nov 2005 14:37:38 +0100 |
wenzelm |
added instance;
|
changeset |
files
|
| Mon, 14 Nov 2005 14:37:15 +0100 |
wenzelm |
added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
|
changeset |
files
|
| Mon, 14 Nov 2005 14:36:46 +0100 |
wenzelm |
Compatibility wrapper for Poly/ML 4.2.0.
|
changeset |
files
|
| Mon, 14 Nov 2005 14:36:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 14 Nov 2005 13:59:58 +0100 |
urbanc |
added a few equivariance lemmas (they need to be automated
|
changeset |
files
|
| Sun, 13 Nov 2005 22:36:30 +0100 |
urbanc |
changed the HOL_basic_ss back and selectively added
|
changeset |
files
|
| Sun, 13 Nov 2005 20:33:36 +0100 |
urbanc |
exchanged HOL_ss for HOL_basic_ss in the simplification
|
changeset |
files
|
| Fri, 11 Nov 2005 10:50:43 +0100 |
chaieb |
a proof step corrected due to the changement in the presburger method.
|
changeset |
files
|
| Fri, 11 Nov 2005 10:49:59 +0100 |
chaieb |
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
|
changeset |
files
|
| Fri, 11 Nov 2005 00:09:37 +0100 |
huffman |
add header
|
changeset |
files
|
| Thu, 10 Nov 2005 21:14:05 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:22 +0100 |
wenzelm |
moved find_free to term.ML;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:21 +0100 |
wenzelm |
guess: Seq.hd;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:20 +0100 |
wenzelm |
guess: Toplevel.proof;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:19 +0100 |
wenzelm |
added find_free (from Isar/proof_context.ML);
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:18 +0100 |
wenzelm |
curried multiply;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:17 +0100 |
wenzelm |
induct method: fixes;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:16 +0100 |
wenzelm |
uncurried Consts.typargs;
|
changeset |
files
|
| Thu, 10 Nov 2005 20:57:11 +0100 |
wenzelm |
renamed Thm.cgoal_of to Thm.cprem_of;
|
changeset |
files
|
| Thu, 10 Nov 2005 17:33:14 +0100 |
paulson |
duplicate axioms in ATP linkup, and general fixes
|
changeset |
files
|
| Thu, 10 Nov 2005 17:31:44 +0100 |
paulson |
tidying
|
changeset |
files
|
| Thu, 10 Nov 2005 00:36:26 +0100 |
urbanc |
called the induction principle "unsafe" instead of "test".
|
changeset |
files
|
| Wed, 09 Nov 2005 18:01:33 +0100 |
paulson |
Skolemization by inference, but not quite finished
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:55 +0100 |
wenzelm |
Explicit data structures for some Isar language elements.
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:53 +0100 |
wenzelm |
tvars_intr_list: natural argument order;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:52 +0100 |
wenzelm |
moved datatype elem to element.ML;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:51 +0100 |
wenzelm |
P.context_element, P.locale_element;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:50 +0100 |
wenzelm |
Element.context;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:49 +0100 |
wenzelm |
use existing exeption Empty;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:48 +0100 |
wenzelm |
avoid code redundancy;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:47 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:46 +0100 |
wenzelm |
removed obsolete term set operations;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:45 +0100 |
wenzelm |
P.locale_element;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:44 +0100 |
wenzelm |
added fold_terms;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:43 +0100 |
wenzelm |
added Isar/element.ML;
|
changeset |
files
|
| Wed, 09 Nov 2005 16:26:41 +0100 |
wenzelm |
Thm.varifyT': natural argument order;
|
changeset |
files
|
| Wed, 09 Nov 2005 12:21:05 +0100 |
haftmann |
added join function
|
changeset |
files
|
| Tue, 08 Nov 2005 15:26:35 +0100 |
haftmann |
allowing indentation of 'theory' keyword
|
changeset |
files
|
| Tue, 08 Nov 2005 10:44:40 +0100 |
wenzelm |
simplified after_qed;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:15 +0100 |
wenzelm |
avoid prove_plain, export_plain, simplified after_qed;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:13 +0100 |
wenzelm |
removed export_plain;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:12 +0100 |
wenzelm |
renamed assert_prop to ensure_prop;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:11 +0100 |
wenzelm |
renamed goals.ML to old_goals.ML;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:10 +0100 |
wenzelm |
export compose_hhf;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:09 +0100 |
wenzelm |
removed impose_hyps, satisfy_hyps;
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:08 +0100 |
wenzelm |
const args: do not store variable names (unused);
|
changeset |
files
|
| Tue, 08 Nov 2005 10:43:05 +0100 |
wenzelm |
renamed goals.ML to old_goals.ML;
|
changeset |
files
|
| Tue, 08 Nov 2005 09:13:22 +0100 |
haftmann |
(fix for accidental commit)
|
changeset |
files
|
| Tue, 08 Nov 2005 09:12:02 +0100 |
haftmann |
(codegen)
|
changeset |
files
|
| Tue, 08 Nov 2005 02:19:11 +0100 |
huffman |
generate pattern combinators for new datatypes
|
changeset |
files
|
| Mon, 07 Nov 2005 23:33:01 +0100 |
huffman |
reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
|
changeset |
files
|
| Mon, 07 Nov 2005 23:30:49 +0100 |
huffman |
add case syntax for type one
|
changeset |
files
|
| Mon, 07 Nov 2005 19:23:53 +0100 |
huffman |
remove syntax for as-patterns
|
changeset |
files
|
| Mon, 07 Nov 2005 19:03:02 +0100 |
wenzelm |
avoid 'as' as identifier;
|
changeset |
files
|
| Mon, 07 Nov 2005 18:50:53 +0100 |
wenzelm |
avoid 'as' as identifier;
|
changeset |
files
|
| Mon, 07 Nov 2005 18:32:54 +0100 |
berghofe |
Added strong induction theorem (currently only axiomatized!).
|
changeset |
files
|
| Mon, 07 Nov 2005 15:19:03 +0100 |
urbanc |
Initial commit.
|
changeset |
files
|
| Mon, 07 Nov 2005 15:12:13 +0100 |
urbanc |
Initial commit of the theory "Weakening".
|
changeset |
files
|
| Mon, 07 Nov 2005 14:35:25 +0100 |
urbanc |
added thms perm, distinct and fresh to the simplifier.
|
changeset |
files
|
| Mon, 07 Nov 2005 12:06:11 +0100 |
haftmann |
added proper fillin_mixfix
|
changeset |
files
|
| Mon, 07 Nov 2005 11:39:24 +0100 |
haftmann |
added fillin_mixfix, replace_quote
|
changeset |
files
|
| Mon, 07 Nov 2005 11:28:34 +0100 |
berghofe |
New function store_thmss_atts.
|
changeset |
files
|
| Mon, 07 Nov 2005 11:17:45 +0100 |
urbanc |
used the function Library.product for the cprod from Stefan
|
changeset |
files
|
| Mon, 07 Nov 2005 10:47:25 +0100 |
urbanc |
fixed bug with nominal induct
|
changeset |
files
|
| Mon, 07 Nov 2005 09:34:51 +0100 |
haftmann |
added fillin_mixfix' needed by serializer
|
changeset |
files
|
| Sun, 06 Nov 2005 01:21:37 +0100 |
huffman |
add case syntax stuff
|
changeset |
files
|
| Sun, 06 Nov 2005 00:35:24 +0100 |
huffman |
use consts for infix syntax
|
changeset |
files
|
| Sun, 06 Nov 2005 00:22:03 +0100 |
huffman |
add proof of Bekic's theorem: fix_cprod
|
changeset |
files
|
| Sat, 05 Nov 2005 21:56:45 +0100 |
huffman |
simplify definitions
|
changeset |
files
|
| Sat, 05 Nov 2005 21:52:13 +0100 |
huffman |
put iterate and fix in separate sections; added Letrec
|
changeset |
files
|
| Sat, 05 Nov 2005 21:50:37 +0100 |
huffman |
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
|
changeset |
files
|
| Sat, 05 Nov 2005 21:42:24 +0100 |
huffman |
add line breaks to Rep_CFun syntax
|
changeset |
files
|
| Fri, 04 Nov 2005 23:15:45 +0100 |
huffman |
moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
|
changeset |
files
|
| Fri, 04 Nov 2005 23:15:11 +0100 |
huffman |
moved adm_chfindom from Fix.thy to Cfun.thy
|
changeset |
files
|
| Fri, 04 Nov 2005 22:27:40 +0100 |
huffman |
cleaned up
|
changeset |
files
|
| Fri, 04 Nov 2005 22:26:09 +0100 |
huffman |
add print translation: Abs_CFun f => LAM x. f x
|
changeset |
files
|
| Thu, 03 Nov 2005 04:31:12 +0100 |
mengj |
Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
|
changeset |
files
|
| Thu, 03 Nov 2005 03:06:02 +0100 |
huffman |
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
|
changeset |
files
|
| Thu, 03 Nov 2005 02:37:09 +0100 |
huffman |
reimplement copy_def to use data constructor constants
|
changeset |
files
|
| Thu, 03 Nov 2005 02:19:48 +0100 |
huffman |
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
|
changeset |
files
|
| Thu, 03 Nov 2005 01:54:51 +0100 |
huffman |
generate lambda pattern syntax for new data constructors
|
changeset |
files
|
| Thu, 03 Nov 2005 01:45:52 +0100 |
huffman |
changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
|
changeset |
files
|
| Thu, 03 Nov 2005 01:44:27 +0100 |
huffman |
add constant one_when; LAM pattern for ONE
|
changeset |
files
|
| Thu, 03 Nov 2005 01:28:22 +0100 |
huffman |
add translation for wildcard pattern
|
changeset |
files
|
| Thu, 03 Nov 2005 01:11:39 +0100 |
huffman |
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
|
changeset |
files
|
| Thu, 03 Nov 2005 01:02:29 +0100 |
huffman |
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
|
changeset |
files
|
| Thu, 03 Nov 2005 00:57:35 +0100 |
huffman |
cleaned up; ch2ch_Rep_CFun is a simp rule
|
changeset |
files
|
| Thu, 03 Nov 2005 00:43:50 +0100 |
huffman |
changed iterate to a continuous type
|
changeset |
files
|
| Thu, 03 Nov 2005 00:43:11 +0100 |
huffman |
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
|
changeset |
files
|
| Thu, 03 Nov 2005 00:32:47 +0100 |
huffman |
removed ex/loeckx.ML
|
changeset |
files
|
| Thu, 03 Nov 2005 00:31:32 +0100 |
huffman |
removed proof about Ifix, which no longer exists
|
changeset |
files
|
| Thu, 03 Nov 2005 00:16:09 +0100 |
huffman |
cleaned up; chain_const and thelub_const are simp rules
|
changeset |
files
|
| Thu, 03 Nov 2005 00:12:29 +0100 |
huffman |
cleaned up; removed adm_tricks in favor of compactness theorems
|
changeset |
files
|
| Wed, 02 Nov 2005 23:59:49 +0100 |
huffman |
fix spelling
|
changeset |
files
|
| Wed, 02 Nov 2005 16:37:39 +0100 |
berghofe |
Moved atom stuff to new file nominal_atoms.ML
|
changeset |
files
|
| Wed, 02 Nov 2005 15:31:12 +0100 |
urbanc |
- completed the list of thms for supp_atm
|
changeset |
files
|
| Wed, 02 Nov 2005 15:05:22 +0100 |
berghofe |
Added code for proving that new datatype has finite support.
|
changeset |
files
|
| Wed, 02 Nov 2005 14:48:55 +0100 |
wenzelm |
removed unused modify_typargs, map_typargs, fold_typargs;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:47:01 +0100 |
wenzelm |
added Isar.state/exn;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:47:00 +0100 |
wenzelm |
Isar.loop;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:58 +0100 |
wenzelm |
moved consts declarations to consts.ML;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:57 +0100 |
wenzelm |
Consts.dest;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:56 +0100 |
wenzelm |
Polymorphic constants.
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:54 +0100 |
wenzelm |
added consts.ML;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:53 +0100 |
wenzelm |
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:51 +0100 |
wenzelm |
dist_eqI: the_context();
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:49 +0100 |
wenzelm |
Sign.const_monomorphic;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:47 +0100 |
wenzelm |
Logic.nth_prem;
|
changeset |
files
|
| Wed, 02 Nov 2005 11:02:29 +0100 |
urbanc |
added the collection of lemmas "supp_at"
|
changeset |
files
|
| Tue, 01 Nov 2005 23:55:53 +0100 |
urbanc |
some minor tweaks in some proofs (nothing extraordinary)
|
changeset |
files
|
| Tue, 01 Nov 2005 23:54:29 +0100 |
urbanc |
tunings of some comments (nothing serious)
|
changeset |
files
|
| Mon, 31 Oct 2005 16:35:15 +0100 |
haftmann |
nth_*, fold_index refined
|
changeset |
files
|
| Mon, 31 Oct 2005 16:00:15 +0100 |
haftmann |
fold_index replacing foldln
|
changeset |
files
|
| Mon, 31 Oct 2005 01:43:22 +0100 |
nipkow |
A few new lemmas
|
changeset |
files
|
| Sun, 30 Oct 2005 10:55:56 +0100 |
urbanc |
tuned my last commit
|
changeset |
files
|
| Sun, 30 Oct 2005 10:37:57 +0100 |
urbanc |
simplified the abs_supp_approx proof and tuned some comments in
|
changeset |
files
|
| Sat, 29 Oct 2005 15:01:25 +0200 |
urbanc |
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
|
changeset |
files
|
| Sat, 29 Oct 2005 14:37:32 +0200 |
urbanc |
1) have adjusted the swapping of the result type
|
changeset |
files
|
| Fri, 28 Oct 2005 22:37:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:32:55 +0200 |
wenzelm |
lthms_containing: not o valid_thms;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:15 +0200 |
wenzelm |
added fact_tac, some_fact_tac;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:13 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:12 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:11 +0200 |
wenzelm |
added fact method;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:09 +0200 |
wenzelm |
tuned ProofContext.export interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:07 +0200 |
wenzelm |
syntax for literal facts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:06 +0200 |
wenzelm |
removed try_dest_Goal, use Logic.unprotect;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:04 +0200 |
wenzelm |
added cgoal_of;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:03 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:02 +0200 |
wenzelm |
export cong_modifiers, simp_modifiers';
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:00 +0200 |
wenzelm |
certify_term: tuned monomorphic consts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:59 +0200 |
wenzelm |
datatype thmref: added Fact;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:58 +0200 |
wenzelm |
Logic.lift_all;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:57 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:56 +0200 |
wenzelm |
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:55 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:54 +0200 |
wenzelm |
added add_local/add_global;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:52 +0200 |
wenzelm |
added incr_indexes;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:51 +0200 |
wenzelm |
renamed Goal constant to prop;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:47 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:46 +0200 |
wenzelm |
Logic.unprotect;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:44 +0200 |
wenzelm |
literal facts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:41 +0200 |
wenzelm |
* Pure/Isar: literal facts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:26:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2005 20:18:37 +0200 |
webertj |
unnecessary imports removed
|
changeset |
files
|
| Fri, 28 Oct 2005 18:53:26 +0200 |
urbanc |
fixed case names in the weak induction principle and
|
changeset |
files
|
| Fri, 28 Oct 2005 18:22:26 +0200 |
berghofe |
Implemented proof of weak induction theorem.
|
changeset |
files
|
| Fri, 28 Oct 2005 17:59:07 +0200 |
berghofe |
Added "deepen" method.
|
changeset |
files
|
| Fri, 28 Oct 2005 17:27:49 +0200 |
haftmann |
circumvented smlnj value restriction
|
changeset |
files
|
| Fri, 28 Oct 2005 17:27:04 +0200 |
haftmann |
added extraction interface for code generator
|
changeset |
files
|
| Fri, 28 Oct 2005 16:43:46 +0200 |
urbanc |
Added (optional) arguments to the tactics
|
changeset |
files
|
| Fri, 28 Oct 2005 16:35:40 +0200 |
haftmann |
cleaned up nth, nth_update, nth_map and nth_string functions
|
changeset |
files
|
| Fri, 28 Oct 2005 13:52:57 +0200 |
berghofe |
Removed legacy prove_goalw_cterm command.
|
changeset |
files
|
| Fri, 28 Oct 2005 12:22:34 +0200 |
paulson |
got rid of obsolete prove_goalw_cterm
|
changeset |
files
|
| Fri, 28 Oct 2005 09:36:19 +0200 |
haftmann |
swapped add_datatype result
|
changeset |
files
|
| Fri, 28 Oct 2005 09:35:04 +0200 |
haftmann |
removed obfuscating PStrStrTab
|
changeset |
files
|
| Fri, 28 Oct 2005 08:40:55 +0200 |
haftmann |
reachable - abandoned foldl_map in favor of fold_map
|
changeset |
files
|
| Fri, 28 Oct 2005 02:30:53 +0200 |
mengj |
Added Tools/res_hol_clause.ML
|
changeset |
files
|
| Fri, 28 Oct 2005 02:30:12 +0200 |
mengj |
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:29:01 +0200 |
mengj |
Added "writeln_strs" to the signature
|
changeset |
files
|
| Fri, 28 Oct 2005 02:28:20 +0200 |
mengj |
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:27:19 +0200 |
mengj |
Added new functions to handle HOL goals and lemmas.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:25:57 +0200 |
mengj |
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:24:58 +0200 |
mengj |
Added several functions to the signature.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:23:49 +0200 |
mengj |
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
|
changeset |
files
|
| Thu, 27 Oct 2005 18:25:33 +0200 |
paulson |
sorted lemma lists
|
changeset |
files
|
| Thu, 27 Oct 2005 13:59:06 +0200 |
wenzelm |
* HOL: alternative iff syntax;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:43 +0200 |
wenzelm |
consts: monomorphic;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:42 +0200 |
wenzelm |
removed inappropriate monomorphic test;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:40 +0200 |
wenzelm |
replaced Defs.monomorphic by Sign.monomorphic;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:38 +0200 |
wenzelm |
alternative iff syntax for equality on booleans, with print_mode 'iff';
|
changeset |
files
|
| Thu, 27 Oct 2005 08:14:05 +0200 |
haftmann |
added module Pure/General/rat.ML
|
changeset |
files
|
| Wed, 26 Oct 2005 16:31:53 +0200 |
paulson |
tidied away duplicate thm
|
changeset |
files
|
| Tue, 25 Oct 2005 18:38:21 +0200 |
wenzelm |
EVERY;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:59 +0200 |
wenzelm |
traceIt: plain term;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:58 +0200 |
wenzelm |
val legacy = ref false;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:57 +0200 |
wenzelm |
prove_raw: cterms, explicit asms;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:49 +0200 |
wenzelm |
avoid legacy goals;
|
changeset |
files
|
| Sat, 22 Oct 2005 01:22:10 +0200 |
wenzelm |
legacy = ref true for the time being -- avoid volumious warnings;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:20:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:17:00 +0200 |
wenzelm |
avoid OldGoals shortcuts;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:16:57 +0200 |
wenzelm |
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
|
changeset |
files
|
| Fri, 21 Oct 2005 18:15:00 +0200 |
wenzelm |
Internal goals.
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:59 +0200 |
wenzelm |
renamed triv_goal to goalI, rev_triv_goal to goalD;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:58 +0200 |
wenzelm |
tuned header;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:57 +0200 |
wenzelm |
Goal.norm_hhf_rule;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:56 +0200 |
wenzelm |
export add_binds_i;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:55 +0200 |
wenzelm |
load_file: setmp OldGoals.legacy true;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:54 +0200 |
wenzelm |
improved check_result;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:53 +0200 |
wenzelm |
Goal.prove_plain;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:52 +0200 |
wenzelm |
do not export find_thms;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:51 +0200 |
wenzelm |
use obsolete goals.ML here;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:50 +0200 |
wenzelm |
Goal.conclude;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:49 +0200 |
wenzelm |
moved SELECT_GOAL to goal.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:48 +0200 |
wenzelm |
moved norm_hhf_rule, prove etc. to goal.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:47 +0200 |
wenzelm |
added simplification tactics and rules (from meta_simplifier.ML);
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:46 +0200 |
wenzelm |
moved various simplification tactics and rules to simplifier.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:45 +0200 |
wenzelm |
warn_obsolete for goal commands -- danger of disrupting a local proof context;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:44 +0200 |
wenzelm |
renamed triv_goal to goalI, rev_triv_goal to goalD;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:43 +0200 |
wenzelm |
added goal.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:42 +0200 |
wenzelm |
added goal.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:41 +0200 |
wenzelm |
Goal.norm_hhf_rule, Goal.init;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:40 +0200 |
wenzelm |
avoid triv_goal and home-grown meta_allE;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:38 +0200 |
wenzelm |
OldGoals;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:37 +0200 |
wenzelm |
proper header;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:36 +0200 |
wenzelm |
avoid home-grown meta_allE;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:34 +0200 |
wenzelm |
Goal.prove;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:32 +0200 |
wenzelm |
avoid shortcuts from OldGoals;
|
changeset |
files
|
| Fri, 21 Oct 2005 16:34:22 +0200 |
wenzelm |
added simplified settings for Poly/ML 4.x (commented out);
|
changeset |
files
|
| Fri, 21 Oct 2005 16:22:59 +0200 |
wenzelm |
reverted (accidental?) change of 1.148;
|
changeset |
files
|
| Fri, 21 Oct 2005 14:49:49 +0200 |
haftmann |
abandoned rational number functions in favor of General/rat.ML
|
changeset |
files
|
| Fri, 21 Oct 2005 14:49:04 +0200 |
haftmann |
introduced functions from Pure/General/rat.ML
|
changeset |
files
|
| Fri, 21 Oct 2005 14:47:37 +0200 |
haftmann |
slight corrections
|
changeset |
files
|
| Fri, 21 Oct 2005 10:32:59 +0200 |
haftmann |
substantially improved integration of website into distribution framework
|
changeset |
files
|
| Fri, 21 Oct 2005 10:32:04 +0200 |
haftmann |
substantially improved integration of website into distribution framework
|
changeset |
files
|
| Fri, 21 Oct 2005 10:27:02 +0200 |
haftmann |
substantially improved integration of website into distribution framework
|
changeset |
files
|
| Fri, 21 Oct 2005 10:21:38 +0200 |
haftmann |
substantially improved integration of website into distribution framework
|
changeset |
files
|
| Fri, 21 Oct 2005 09:54:03 +0200 |
haftmann |
towards an improved website/makedist integration
|
changeset |
files
|
| Fri, 21 Oct 2005 09:18:27 +0200 |
haftmann |
towards an improved website/makedist integration
|
changeset |
files
|
| Fri, 21 Oct 2005 09:08:42 +0200 |
haftmann |
added default distinfo.mak
|
changeset |
files
|
| Fri, 21 Oct 2005 09:05:52 +0200 |
haftmann |
towards an improved website/makedist integration
|
changeset |
files
|
| Fri, 21 Oct 2005 09:05:52 +0200 |
haftmann |
towards an improved website/makedist integration
|
changeset |
files
|
| Fri, 21 Oct 2005 08:23:45 +0200 |
haftmann |
added rounding functions
|
changeset |
files
|
| Fri, 21 Oct 2005 02:57:22 +0200 |
mengj |
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
|
changeset |
files
|
| Wed, 19 Oct 2005 21:53:34 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:50 +0200 |
wenzelm |
removed add_inductive_x;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:49 +0200 |
wenzelm |
removed obsolete add_datatype_x;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:48 +0200 |
wenzelm |
removed obsolete thy_syntax.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:47 +0200 |
wenzelm |
removed obsolete old_symbol_source;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:46 +0200 |
wenzelm |
removed obsolete non-Isar theory format and old Isar theory headers;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:45 +0200 |
wenzelm |
removed old-style theory format;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:44 +0200 |
wenzelm |
avoid lagacy read function;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:43 +0200 |
wenzelm |
added thm(s) retrieval functions (from goals.ML);
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:42 +0200 |
wenzelm |
removed obsolete old-locales;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:41 +0200 |
wenzelm |
removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:40 +0200 |
wenzelm |
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:38 +0200 |
wenzelm |
removed obsolete old-style syntax;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:37 +0200 |
wenzelm |
removed obsolete IOA/meta_theory/ioa_package.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:36 +0200 |
wenzelm |
removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:35 +0200 |
wenzelm |
removed obsolete domain/interface.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:34 +0200 |
wenzelm |
removed obsolete add_typedef_x;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:33 +0200 |
wenzelm |
removed print_exn (better let the toplevel do this);
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:32 +0200 |
wenzelm |
removed obsolete add_recdef_old;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:31 +0200 |
wenzelm |
removed obsolete HOL/thy_syntax.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:30 +0200 |
wenzelm |
* Theory syntax: discontinued non-Isar format and old Isar headers;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:29 +0200 |
wenzelm |
replaced commafy by existing commas;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:28 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:27 +0200 |
wenzelm |
isatool fixheaders;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:07 +0200 |
wenzelm |
fix headers;
|
changeset |
files
|
| Wed, 19 Oct 2005 17:21:53 +0200 |
haftmann |
added table functor instance for pairs of strings
|
changeset |
files
|
| Wed, 19 Oct 2005 17:19:52 +0200 |
haftmann |
added subgraph
|
changeset |
files
|
| Wed, 19 Oct 2005 17:19:37 +0200 |
haftmann |
added join
|
changeset |
files
|
| Wed, 19 Oct 2005 16:32:09 +0200 |
haftmann |
slight improvements for website
|
changeset |
files
|
| Wed, 19 Oct 2005 14:51:12 +0200 |
wenzelm |
moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!
|
changeset |
files
|
| Wed, 19 Oct 2005 13:59:33 +0200 |
mengj |
More functions are added to the signature of ResClause
|
changeset |
files
|
| Wed, 19 Oct 2005 10:25:46 +0200 |
mengj |
*** empty log message ***
|
changeset |
files
|
| Wed, 19 Oct 2005 06:46:45 +0200 |
nipkow |
added 2 lemmas
|
changeset |
files
|
| Wed, 19 Oct 2005 06:33:24 +0200 |
mengj |
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:37 +0200 |
wenzelm |
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:36 +0200 |
wenzelm |
tuned error msg;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:35 +0200 |
wenzelm |
renamed atomize_rule to atomize_cterm;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:34 +0200 |
wenzelm |
ObjectLogic.atomize_cterm;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:33 +0200 |
wenzelm |
use simplified Toplevel.proof etc.;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:32 +0200 |
wenzelm |
back: Toplevel.actual/skip_proof;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:31 +0200 |
wenzelm |
renamed set_context to context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:30 +0200 |
wenzelm |
renamed set_context to context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:29 +0200 |
wenzelm |
functor: no Simplifier argument;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:28 +0200 |
wenzelm |
moved helper lemma to HilbertChoice.thy;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:27 +0200 |
wenzelm |
Simplifier.theory_context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:26 +0200 |
wenzelm |
added lemma exE_some (from specification_package.ML);
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:25 +0200 |
wenzelm |
Simplifier.theory_context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:24 +0200 |
wenzelm |
tuned error msg;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:23 +0200 |
wenzelm |
Simplifier.context/theory_context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:22 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 18 Oct 2005 15:08:38 +0200 |
paulson |
new interface to make_conjecture_clauses
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:25 +0200 |
wenzelm |
* Simplifier: simpset of a running simplification process contains a proof context;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:24 +0200 |
wenzelm |
added type_solver (uses Simplifier.the_context);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:23 +0200 |
wenzelm |
added pos/negDivAlg_induct declarations (from Main.thy);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:22 +0200 |
wenzelm |
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:21 +0200 |
wenzelm |
removed obsolete/experimental context components (superceded by Simplifier.the_context);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:20 +0200 |
wenzelm |
added set/addloop' for simpset dependent loopers;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:19 +0200 |
wenzelm |
functor: no Simplifier argument;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:18 +0200 |
wenzelm |
change_claset(_of): more abtract interface;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:17 +0200 |
wenzelm |
functor: no Simplifier argument;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:15 +0200 |
wenzelm |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:13 +0200 |
wenzelm |
change_claset/simpset;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:10 +0200 |
wenzelm |
change_claset/simpset;
|
changeset |
files
|
| Mon, 17 Oct 2005 19:19:29 +0200 |
berghofe |
Improved proof of injectivity theorems to make it work on
|
changeset |
files
|
| Mon, 17 Oct 2005 18:34:51 +0200 |
berghofe |
Fixed bug in proof of support theorem (it failed on constructors with no arguments).
|
changeset |
files
|
| Mon, 17 Oct 2005 17:42:24 +0200 |
berghofe |
Implemented proofs for support and freshness theorems.
|
changeset |
files
|
| Mon, 17 Oct 2005 17:40:34 +0200 |
urbanc |
deleted leading space in the definition of fresh
|
changeset |
files
|
| Mon, 17 Oct 2005 12:30:57 +0200 |
berghofe |
Initial revision.
|
changeset |
files
|
| Sat, 15 Oct 2005 00:14:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:09:20 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:09:07 +0200 |
wenzelm |
added ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:15 +0200 |
wenzelm |
more;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:14 +0200 |
wenzelm |
* antiquotations ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:13 +0200 |
wenzelm |
added guess;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:12 +0200 |
wenzelm |
added antiquotations ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:11 +0200 |
wenzelm |
use perl for test/stat;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:10 +0200 |
wenzelm |
export strip_params;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:09 +0200 |
wenzelm |
note_thmss, read/cert_vars etc.: natural argument order;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:08 +0200 |
wenzelm |
goal statements: before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:07 +0200 |
wenzelm |
added 'guess', which derives the obtained context from the course of reasoning;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:06 +0200 |
wenzelm |
added primitive_text, succeed_text;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:05 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:04 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:03 +0200 |
wenzelm |
added 'guess';
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:01 +0200 |
wenzelm |
added no_facts;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:00 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:07:59 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 14 Oct 2005 15:34:56 +0200 |
paulson |
signature changes
|
changeset |
files
|
| Fri, 14 Oct 2005 14:36:39 +0200 |
haftmann |
added module rat.ML for rational numbers
|
changeset |
files
|
| Fri, 14 Oct 2005 13:04:38 +0200 |
isatest |
longer time out for test (kleing)
|
changeset |
files
|
| Fri, 14 Oct 2005 11:36:14 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
changeset |
files
|
| Fri, 14 Oct 2005 10:19:50 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
changeset |
files
|
| Thu, 13 Oct 2005 11:58:22 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Wed, 12 Oct 2005 18:17:48 +0200 |
webertj |
counter added to SAT signature
|
changeset |
files
|
| Wed, 12 Oct 2005 17:06:22 +0200 |
webertj |
no proof reconstruction when quick_and_dirty is set
|
changeset |
files
|
| Wed, 12 Oct 2005 10:49:07 +0200 |
paulson |
tidying
|
changeset |
files
|
| Wed, 12 Oct 2005 03:02:18 +0200 |
huffman |
domain package generates compactness lemmas for new constructors
|
changeset |
files
|
| Wed, 12 Oct 2005 03:01:30 +0200 |
huffman |
add ML bindings for compactness lemmas
|
changeset |
files
|
| Wed, 12 Oct 2005 03:01:09 +0200 |
huffman |
added compactness theorems
|
changeset |
files
|
| Wed, 12 Oct 2005 01:43:37 +0200 |
huffman |
added compactness lemmas; cleaned up
|
changeset |
files
|
| Tue, 11 Oct 2005 23:47:29 +0200 |
huffman |
added compactness theorems in locale iso
|
changeset |
files
|
| Tue, 11 Oct 2005 23:27:49 +0200 |
huffman |
added several theorems in locale iso
|
changeset |
files
|
| Tue, 11 Oct 2005 23:27:14 +0200 |
huffman |
added xsymbols syntax for pairs; cleaned up
|
changeset |
files
|
| Tue, 11 Oct 2005 23:23:39 +0200 |
huffman |
added theorem typedef_compact
|
changeset |
files
|
| Tue, 11 Oct 2005 23:22:12 +0200 |
huffman |
rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less
|
changeset |
files
|
| Tue, 11 Oct 2005 23:19:50 +0200 |
huffman |
cleaned up; renamed less_fun to expand_fun_less
|
changeset |
files
|
| Tue, 11 Oct 2005 17:30:00 +0200 |
nipkow |
added hd lemma
|
changeset |
files
|
| Tue, 11 Oct 2005 15:04:11 +0200 |
paulson |
simplifying the treatment of clausification
|
changeset |
files
|
| Tue, 11 Oct 2005 15:03:36 +0200 |
paulson |
simplifying the treatment of nameless theorems
|
changeset |
files
|
| Tue, 11 Oct 2005 14:02:33 +0200 |
wenzelm |
expand: error on undefined/empty env variable;
|
changeset |
files
|
| Tue, 11 Oct 2005 14:02:32 +0200 |
wenzelm |
added assert;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:30:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:08 +0200 |
wenzelm |
added string_of_pid;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:07 +0200 |
wenzelm |
raw symbols: allow non-ASCII chars (e.g. UTF-8);
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:06 +0200 |
wenzelm |
moved string_of_pid to ML-Systems;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:05 +0200 |
wenzelm |
ML_SUFFIX in targets (experimental);
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:04 +0200 |
wenzelm |
cleanup backup images;
|
changeset |
files
|
| Mon, 10 Oct 2005 15:35:29 +0200 |
paulson |
small tidy-up of utility functions
|
changeset |
files
|
| Mon, 10 Oct 2005 14:43:45 +0200 |
wenzelm |
updated print_tac;
|
changeset |
files
|
| Mon, 10 Oct 2005 05:46:17 +0200 |
huffman |
add names to infix declarations
|
changeset |
files
|
| Mon, 10 Oct 2005 05:30:02 +0200 |
huffman |
new syntax translations for continuous lambda abstraction
|
changeset |
files
|
| Mon, 10 Oct 2005 04:38:26 +0200 |
huffman |
removed Istrictify; simplified some proofs
|
changeset |
files
|
| Mon, 10 Oct 2005 04:12:31 +0200 |
huffman |
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
|
changeset |
files
|
| Mon, 10 Oct 2005 04:03:09 +0200 |
huffman |
cleaned up
|
changeset |
files
|
| Mon, 10 Oct 2005 04:00:40 +0200 |
huffman |
added theorem typedef_chfin
|
changeset |
files
|
| Mon, 10 Oct 2005 03:55:39 +0200 |
huffman |
replaced foldr' with foldr1
|
changeset |
files
|
| Mon, 10 Oct 2005 03:47:00 +0200 |
huffman |
cleaned up; renamed "Porder.op <<" to "Porder.<<"
|
changeset |
files
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
changeset |
files
|
| Sat, 08 Oct 2005 23:43:15 +0200 |
wenzelm |
tuned Memory.hilim;
|
changeset |
files
|
| Sat, 08 Oct 2005 23:43:14 +0200 |
wenzelm |
get rid of feeder -- at the cost of batch-only commit-at-exit;
|
changeset |
files
|
| Sat, 08 Oct 2005 23:36:01 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Sat, 08 Oct 2005 23:05:59 +0200 |
wenzelm |
-nort option;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:42 +0200 |
wenzelm |
added could_unify;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:41 +0200 |
wenzelm |
more efficient check_specified, much less invocations;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:40 +0200 |
wenzelm |
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:39 +0200 |
wenzelm |
uses susp.ML, lazy_seq.ML, lazy_scan.ML;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:38 +0200 |
wenzelm |
added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:38 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:37 +0200 |
wenzelm |
tuned memory limits;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:36 +0200 |
wenzelm |
Int.max;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:35 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:34 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:33 +0200 |
wenzelm |
initial pop11 code for ML use/use_string;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:32 +0200 |
wenzelm |
Poplog/PML: ML_SUFFIX=.psv;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:31 +0200 |
wenzelm |
support ML_SUFFIX;
|
changeset |
files
|
| Sat, 08 Oct 2005 18:51:03 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sat, 08 Oct 2005 15:20:58 +0200 |
nipkow |
fix due to new neq_simproc
|
changeset |
files
|
| Fri, 07 Oct 2005 23:29:00 +0200 |
wenzelm |
removed obsolete comment;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:26 +0200 |
wenzelm |
added idtypdummy_ast_tr;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:25 +0200 |
wenzelm |
added syntax for _idtdummy, _idtypdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:24 +0200 |
wenzelm |
added absdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:23 +0200 |
wenzelm |
removed obsolete dummy_pat_tr;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:22 +0200 |
wenzelm |
Term.absdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:21 +0200 |
wenzelm |
removed obsolete ex/Tuple.thy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:19 +0200 |
wenzelm |
replaced _K by dummy abstraction;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:18 +0200 |
wenzelm |
print_translation: does not handle _idtdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:15 +0200 |
wenzelm |
added dummy variable binding;
|
changeset |
files
|
| Fri, 07 Oct 2005 20:41:10 +0200 |
nipkow |
changes due to new neq_simproc in simpdata.ML
|
changeset |
files
|
| Fri, 07 Oct 2005 18:49:20 +0200 |
wenzelm |
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
|
changeset |
files
|
| Fri, 07 Oct 2005 18:49:19 +0200 |
wenzelm |
Term.str_of_term;
|
changeset |
files
|
| Fri, 07 Oct 2005 17:57:21 +0200 |
paulson |
minor code tidyig
|
changeset |
files
|
| Fri, 07 Oct 2005 15:08:28 +0200 |
paulson |
code restructuring
|
changeset |
files
|
| Fri, 07 Oct 2005 11:29:24 +0200 |
paulson |
more tidying. Fixed process management bugs and race condition
|
changeset |
files
|
| Thu, 06 Oct 2005 10:14:22 +0200 |
paulson |
major simplification: removal of the goalstring argument
|
changeset |
files
|
| Thu, 06 Oct 2005 10:13:34 +0200 |
berghofe |
Optimized getPreds and getSuccs.
|
changeset |
files
|
| Thu, 06 Oct 2005 08:58:58 +0200 |
haftmann |
adjusted sydney to new website
|
changeset |
files
|
| Thu, 06 Oct 2005 08:56:15 +0200 |
haftmann |
changed sydney share
|
changeset |
files
|
| Wed, 05 Oct 2005 19:28:12 +0200 |
wenzelm |
added Poplog/PML version 15.6/2.1 (experimental!);
|
changeset |
files
|
| Wed, 05 Oct 2005 18:38:43 +0200 |
haftmann |
added fold_nodes, map_node_yield
|
changeset |
files
|
| Wed, 05 Oct 2005 18:38:28 +0200 |
haftmann |
added merge, tuned
|
changeset |
files
|
| Wed, 05 Oct 2005 14:01:32 +0200 |
nipkow |
added last in set lemma
|
changeset |
files
|
| Wed, 05 Oct 2005 11:18:06 +0200 |
paulson |
improved process handling. tidied
|
changeset |
files
|
| Wed, 05 Oct 2005 10:56:06 +0200 |
paulson |
more signals
|
changeset |
files
|
| Tue, 04 Oct 2005 23:39:42 +0200 |
nipkow |
new hd/rev/last lemmas
|
changeset |
files
|
| Tue, 04 Oct 2005 23:30:46 +0200 |
nipkow |
new lemmas
|
changeset |
files
|
| Tue, 04 Oct 2005 21:39:16 +0200 |
wenzelm |
added compiler and runtime options;
|
changeset |
files
|
| Tue, 04 Oct 2005 21:33:09 +0200 |
wenzelm |
Poplog/PML startup script.
|
changeset |
files
|
| Tue, 04 Oct 2005 20:38:13 +0200 |
wenzelm |
Compatibility file for Poplog/PML (version 15.6/2.1).
|
changeset |
files
|
| Tue, 04 Oct 2005 19:05:37 +0200 |
wenzelm |
Substring.all = Substring.full;
|
changeset |
files
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
changeset |
files
|
| Tue, 04 Oct 2005 16:47:40 +0200 |
wenzelm |
find_theorems: support * wildcard in name: criterion;
|
changeset |
files
|
| Tue, 04 Oct 2005 16:47:39 +0200 |
wenzelm |
* Command 'find_theorems': support * wildcard in name: criterion.
|
changeset |
files
|
| Tue, 04 Oct 2005 16:05:08 +0200 |
wenzelm |
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
|
changeset |
files
|
| Tue, 04 Oct 2005 14:58:44 +0200 |
haftmann |
added redirect.html
|
changeset |
files
|
| Tue, 04 Oct 2005 14:37:06 +0200 |
haftmann |
better error handling
|
changeset |
files
|
| Tue, 04 Oct 2005 11:15:09 +0200 |
haftmann |
improved linktest
|
changeset |
files
|
| Tue, 04 Oct 2005 10:58:46 +0200 |
haftmann |
removed removed IntFloor
|
changeset |
files
|
| Tue, 04 Oct 2005 10:55:14 +0200 |
haftmann |
fixed broken link
|
changeset |
files
|
| Tue, 04 Oct 2005 10:52:43 +0200 |
haftmann |
fixed broken mailto: link
|
changeset |
files
|
| Tue, 04 Oct 2005 09:59:01 +0200 |
paulson |
fixed the ascii-armouring of goalstring
|
changeset |
files
|
| Tue, 04 Oct 2005 09:58:38 +0200 |
paulson |
reset clause counter
|
changeset |
files
|
| Tue, 04 Oct 2005 09:58:17 +0200 |
paulson |
theorems need names
|
changeset |
files
|
| Tue, 04 Oct 2005 09:19:17 +0200 |
haftmann |
support for setting local permissions
|
changeset |
files
|
| Tue, 04 Oct 2005 08:49:24 +0200 |
haftmann |
improved dependency build
|
changeset |
files
|
| Tue, 04 Oct 2005 08:14:15 +0200 |
haftmann |
added conf/ to .cvsignore
|
changeset |
files
|
| Fri, 30 Sep 2005 18:18:34 +0200 |
aspinall |
Add icon for interface.
Isabelle2005
|
changeset |
files
|
| Fri, 30 Sep 2005 17:54:04 +0200 |
aspinall |
Move welcomemsg and helpdoc to pgip_isar.xml
|
changeset |
files
|
| Fri, 30 Sep 2005 17:52:18 +0200 |
aspinall |
Add helpdocs and welcomemsg here instead of hard wiring in proof_general.ML.
|
changeset |
files
|
| Fri, 30 Sep 2005 17:33:22 +0200 |
aspinall |
Explanatory text
|
changeset |
files
|
| Fri, 30 Sep 2005 17:28:04 +0200 |
aspinall |
Schema files (for information, and validating pgip_isar.xml)
|
changeset |
files
|
| Fri, 30 Sep 2005 17:24:51 +0200 |
aspinall |
Schema for PGIP
|
changeset |
files
|
| Fri, 30 Sep 2005 15:28:43 +0200 |
wenzelm |
pruned notes about Poly/ML;
|
changeset |
files
|
| Fri, 30 Sep 2005 15:17:04 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Fri, 30 Sep 2005 13:47:36 +0200 |
aspinall |
Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
|
changeset |
files
|
| Fri, 30 Sep 2005 11:43:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 30 Sep 2005 10:58:11 +0200 |
aspinall |
Fix for guiconfig -> displayconfig element rename
|
changeset |
files
|
| Fri, 30 Sep 2005 09:52:46 +0200 |
paulson |
theorems need names
|
changeset |
files
|
| Thu, 29 Sep 2005 19:37:20 +0200 |
wenzelm |
refer to $PRG instead of (old) rsync-isabelle;
|
changeset |
files
|
| Thu, 29 Sep 2005 18:01:12 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:09:11 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:08:52 +0200 |
wenzelm |
pdfsetup.sty: better not rely on ifpdf.sty;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:02:57 +0200 |
paulson |
simprules need names
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:46 +0200 |
wenzelm |
export debug_bounds;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:45 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:44 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:43 +0200 |
wenzelm |
Isabelle2005 (October 2005);
|
changeset |
files
|
| Thu, 29 Sep 2005 15:31:34 +0200 |
nipkow |
Added a few lemmas
|
changeset |
files
|
| Thu, 29 Sep 2005 12:45:16 +0200 |
paulson |
reduction in tracing files
|
changeset |
files
|
| Thu, 29 Sep 2005 12:45:04 +0200 |
paulson |
improvements for problem generation
|
changeset |
files
|
| Thu, 29 Sep 2005 12:44:25 +0200 |
paulson |
moved concat_with_and to watcher.ML
|
changeset |
files
|
| Thu, 29 Sep 2005 12:43:40 +0200 |
paulson |
a name for empty_not_insert
|
changeset |
files
|
| Thu, 29 Sep 2005 12:33:26 +0200 |
berghofe |
Simplifier now removes flex-flex constraints from theorem returned by prover.
|
changeset |
files
|
| Thu, 29 Sep 2005 12:30:30 +0200 |
berghofe |
Optimized and exported flexflex_unique.
|
changeset |
files
|
| Thu, 29 Sep 2005 01:12:16 +0200 |
wenzelm |
make signature constraint actually work;
|
changeset |
files
|
| Thu, 29 Sep 2005 01:09:39 +0200 |
wenzelm |
activate signature constraints;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:03 +0200 |
wenzelm |
HOL4 image is back;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:02 +0200 |
wenzelm |
tuned default operation: use internal modify;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:01 +0200 |
wenzelm |
abstract_rule: tuned exception msgs;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:00 +0200 |
wenzelm |
back to simple 'defs' (cf. revision 1.79 of theory.ML);
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:59 +0200 |
wenzelm |
back to simple 'defs' (cf. revision 1.79);
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:58 +0200 |
wenzelm |
removed revert_bound;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:57 +0200 |
wenzelm |
print_theory: discontinued final consts;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:56 +0200 |
wenzelm |
Theory.add_finals_i;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:55 +0200 |
wenzelm |
more finalconsts;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 28 Sep 2005 18:50:42 +0200 |
webertj |
pointer to HOL/ex/SAT_Examples.thy added
|
changeset |
files
|
| Wed, 28 Sep 2005 16:58:06 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 28 Sep 2005 15:13:02 +0200 |
wenzelm |
more reliable check for PDF output using ifpdf.sty;
|
changeset |
files
|
| Wed, 28 Sep 2005 14:41:43 +0200 |
webertj |
pre_sat_tac moved towards end of file
|
changeset |
files
|
| Wed, 28 Sep 2005 14:16:34 +0200 |
haftmann |
adjusted www links
|
changeset |
files
|
| Wed, 28 Sep 2005 14:16:12 +0200 |
webertj |
comment fixed
|
changeset |
files
|
| Wed, 28 Sep 2005 13:17:23 +0200 |
obua |
mapped "-->" to "hol4-->"
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:15 +0200 |
wenzelm |
avoid naming existing tags in explanations;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:14 +0200 |
wenzelm |
revert 'defs' advertisement;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:13 +0200 |
wenzelm |
revert 'defs' advertisement;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:16:27 +0200 |
paulson |
time limit option; fixed bug concerning first line of ATP output
|
changeset |
files
|
| Wed, 28 Sep 2005 11:15:33 +0200 |
paulson |
streamlined theory; conformance to recent publication
|
changeset |
files
|
| Wed, 28 Sep 2005 11:14:26 +0200 |
paulson |
new lemma
|
changeset |
files
|
| Wed, 28 Sep 2005 09:14:44 +0200 |
haftmann |
better appearance in lynx and netscape4
|
changeset |
files
|
| Wed, 28 Sep 2005 08:57:19 +0200 |
haftmann |
MB instead of KB
|
changeset |
files
|
| Tue, 27 Sep 2005 20:43:39 +0200 |
wenzelm |
renamed packages to download;
|
changeset |
files
|
| Tue, 27 Sep 2005 17:24:27 +0200 |
wenzelm |
more details about incomplete 'defs';
|
changeset |
files
|
| Tue, 27 Sep 2005 17:14:27 +0200 |
wenzelm |
renamed "Packages" to "Download";
|
changeset |
files
|
| Tue, 27 Sep 2005 17:13:11 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:09:46 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:09:46 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:03:54 +0200 |
haftmann |
slight corrections
|
changeset |
files
|
| Tue, 27 Sep 2005 17:01:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 27 Sep 2005 17:01:10 +0200 |
wenzelm |
renamed "Packages" to "Download";
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:38 +0200 |
haftmann |
fixed dead link
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:38 +0200 |
haftmann |
fixed dead link
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:24 +0200 |
haftmann |
improved linkcheck
|
changeset |
files
|
| Tue, 27 Sep 2005 16:33:36 +0200 |
haftmann |
added simple linktester for isabelle website
|
changeset |
files
|
| Tue, 27 Sep 2005 16:28:11 +0200 |
wenzelm |
warn about Poly/ML segfault problem;
|
changeset |
files
|
| Tue, 27 Sep 2005 15:30:37 +0200 |
haftmann |
website preparation for Isabelle2005
|
changeset |
files
|
| Tue, 27 Sep 2005 14:41:41 +0200 |
obua |
corrected spelling bug
|
changeset |
files
|
| Tue, 27 Sep 2005 14:39:35 +0200 |
obua |
added defs disclaimer
|
changeset |
files
|
| Tue, 27 Sep 2005 12:16:06 +0200 |
berghofe |
nat_number_of is no longer declared as code lemma, since this turned
|
changeset |
files
|
| Tue, 27 Sep 2005 12:14:39 +0200 |
berghofe |
Inserted clause for nat in number_of_codegen again ("code unfold" turned
|
changeset |
files
|
| Tue, 27 Sep 2005 12:13:17 +0200 |
berghofe |
Optimized unfold_attr.
|
changeset |
files
|
| Tue, 27 Sep 2005 11:39:27 +0200 |
wenzelm |
removed link to HOL4, which is not in the library right now;
|
changeset |
files
|
| Tue, 27 Sep 2005 11:27:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 27 Sep 2005 11:03:38 +0200 |
berghofe |
Added entries for code_module, code_library, and value.
|
changeset |
files
|
| Tue, 27 Sep 2005 11:02:16 +0200 |
berghofe |
Tuned.
|
changeset |
files
|
| Mon, 26 Sep 2005 20:52:36 +0200 |
wenzelm |
updates for Isabelle2005;
|
changeset |
files
|
| Mon, 26 Sep 2005 20:51:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 26 Sep 2005 20:12:51 +0200 |
berghofe |
Updated description of code generator.
|
changeset |
files
|
| Mon, 26 Sep 2005 19:19:15 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Mon, 26 Sep 2005 19:19:14 +0200 |
wenzelm |
moved disambiguate_frees to ProofKernel;
|
changeset |
files
|
| Mon, 26 Sep 2005 19:19:13 +0200 |
wenzelm |
quote 'value';
|
changeset |
files
|
| Mon, 26 Sep 2005 19:19:12 +0200 |
wenzelm |
yet another atempt to get doc/Contents right;
|
changeset |
files
|
| Mon, 26 Sep 2005 19:04:31 +0200 |
berghofe |
Renamed wf_rec to wfrec in consts_code declaration.
|
changeset |
files
|
| Mon, 26 Sep 2005 17:14:48 +0200 |
wenzelm |
really copy doc/Contents;
|
changeset |
files
|
| Mon, 26 Sep 2005 16:10:19 +0200 |
obua |
Release HOL4 and HOLLight Importer.
|
changeset |
files
|
| Mon, 26 Sep 2005 15:56:28 +0200 |
wenzelm |
copy doc/Contents;
|
changeset |
files
|
| Mon, 26 Sep 2005 15:17:33 +0200 |
skalberg |
Made sure all lemmas now have names (especially so that certain of them
|
changeset |
files
|
| Mon, 26 Sep 2005 13:12:24 +0200 |
wenzelm |
echo HOL_USERDIR_OPTIONS;
|
changeset |
files
|
| Mon, 26 Sep 2005 08:50:21 +0200 |
obua |
tuned
|
changeset |
files
|
| Mon, 26 Sep 2005 08:49:50 +0200 |
obua |
added ROOT.ML
|
changeset |
files
|
| Mon, 26 Sep 2005 08:41:24 +0200 |
haftmann |
adjusted web link
|
changeset |
files
|
| Mon, 26 Sep 2005 02:27:59 +0200 |
obua |
added entry for running HOLLight
|
changeset |
files
|
| Mon, 26 Sep 2005 02:27:14 +0200 |
obua |
fixed disambiguation problem
|
changeset |
files
|
| Mon, 26 Sep 2005 02:06:44 +0200 |
obua |
added Drule.disambiguate_frees : thm -> thm
|
changeset |
files
|
| Sun, 25 Sep 2005 23:36:14 +0200 |
wenzelm |
zero_var_inst: replace loose bounds :000 etc.;
|
changeset |
files
|
| Sun, 25 Sep 2005 20:24:23 +0200 |
wenzelm |
* Hyperreal: A theory of Taylor series.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:24:10 +0200 |
wenzelm |
more;
|
changeset |
files
|
| Sun, 25 Sep 2005 20:19:31 +0200 |
berghofe |
eq_codegen now ensures that code for bool type is generated.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:17:44 +0200 |
berghofe |
Fixed print mode problem in test_term.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:17:13 +0200 |
berghofe |
Added ExecutableSet and Taylor.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:15:29 +0200 |
berghofe |
Now uses set implementation from ExecutableSet.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:14:39 +0200 |
berghofe |
Added Taylor.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:14:16 +0200 |
berghofe |
Formalization of Taylor series by Lukas Bulwahn and
|
changeset |
files
|
| Sun, 25 Sep 2005 20:12:59 +0200 |
berghofe |
Added ExecutableSet.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:12:26 +0200 |
berghofe |
New theory for implementing finite sets by lists.
|
changeset |
files
|
| Sun, 25 Sep 2005 01:12:49 +0200 |
webertj |
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
|
changeset |
files
|
| Sat, 24 Sep 2005 23:55:17 +0200 |
obua |
set show_types and show_sorts during import
|
changeset |
files
|
| Sat, 24 Sep 2005 21:13:15 +0200 |
nipkow |
a few new filter lemmas
|
changeset |
files
|
| Sat, 24 Sep 2005 16:43:41 +0200 |
obua |
HOL4-Import: map ONTO to Fun.surj
|
changeset |
files
|
| Sat, 24 Sep 2005 13:54:35 +0200 |
webertj |
cnf_struct renamed to cnf
|
changeset |
files
|
| Sat, 24 Sep 2005 13:26:40 +0200 |
obua |
remove debug clutter
|
changeset |
files
|
| Sat, 24 Sep 2005 13:11:05 +0200 |
obua |
preliminary fix of HOL build problem
|
changeset |
files
|
| Sat, 24 Sep 2005 10:47:22 +0200 |
obua |
bug fix
|
changeset |
files
|
| Sat, 24 Sep 2005 07:57:50 +0200 |
webertj |
replay_proof optimized: now performs backwards proof search
|
changeset |
files
|
| Sat, 24 Sep 2005 07:21:46 +0200 |
webertj |
code reformatted and restructured, many minor modifications
|
changeset |
files
|
| Sat, 24 Sep 2005 07:10:57 +0200 |
webertj |
bugfix in "zchaff_with_proofs"
|
changeset |
files
|
| Sat, 24 Sep 2005 02:53:08 +0200 |
webertj |
parse_std_result_file renamed to read_std_result_file
|
changeset |
files
|
| Fri, 23 Sep 2005 23:28:59 +0200 |
webertj |
new sat tactic
|
changeset |
files
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
changeset |
files
|
| Fri, 23 Sep 2005 22:49:25 +0200 |
obua |
fix
|
changeset |
files
|
| Fri, 23 Sep 2005 22:31:22 +0200 |
wenzelm |
simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:55 +0200 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:54 +0200 |
wenzelm |
added mk_solver';
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:53 +0200 |
wenzelm |
Simplifier.inherit_bounds;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:52 +0200 |
wenzelm |
adm_tac/cont_tacRs: proper simpset;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:51 +0200 |
wenzelm |
Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:50 +0200 |
wenzelm |
tuned order of targets;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:49 +0200 |
wenzelm |
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
|
changeset |
files
|
| Fri, 23 Sep 2005 21:02:13 +0200 |
webertj |
some typos in comments fixed
|
changeset |
files
|
| Fri, 23 Sep 2005 20:13:54 +0200 |
obua |
1) fixed bug in type_introduction: first stage uses different namespace than second stage
|
changeset |
files
|
| Fri, 23 Sep 2005 18:47:47 +0200 |
wenzelm |
removed doc/index.html from distribution (now produced by website);
|
changeset |
files
|
| Fri, 23 Sep 2005 17:06:23 +0200 |
haftmann |
mkdir -p for symlinks
|
changeset |
files
|
| Fri, 23 Sep 2005 16:05:42 +0200 |
nipkow |
rules -> iprover
|
changeset |
files
|
| Fri, 23 Sep 2005 16:05:10 +0200 |
webertj |
spaces inserted in header
|
changeset |
files
|
| Fri, 23 Sep 2005 16:01:45 +0200 |
webertj |
header (title/ID) added
|
changeset |
files
|
| Fri, 23 Sep 2005 15:45:12 +0200 |
webertj |
typo fixed: rufute -> refute
|
changeset |
files
|
| Fri, 23 Sep 2005 15:38:22 +0200 |
schirmer |
bugfix in record_tr'
|
changeset |
files
|
| Fri, 23 Sep 2005 15:32:42 +0200 |
wenzelm |
method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;
|
changeset |
files
|
| Fri, 23 Sep 2005 14:55:28 +0200 |
wenzelm |
Id;
|
changeset |
files
|
| Fri, 23 Sep 2005 13:20:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 23 Sep 2005 10:26:07 +0200 |
paulson |
changed defaults
|
changeset |
files
|
| Fri, 23 Sep 2005 10:25:55 +0200 |
paulson |
ATP linkup
|
changeset |
files
|
| Fri, 23 Sep 2005 10:01:14 +0200 |
obua |
replay type_introduction fix
|
changeset |
files
|
| Fri, 23 Sep 2005 09:00:19 +0200 |
haftmann |
temporarily re-introduced overwrite_warn
|
changeset |
files
|
| Fri, 23 Sep 2005 00:52:13 +0200 |
obua |
add debug messages
|
changeset |
files
|
| Fri, 23 Sep 2005 00:11:10 +0200 |
nipkow |
renamed rules to iprover
|
changeset |
files
|
| Fri, 23 Sep 2005 00:10:58 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
changeset |
files
|
| Thu, 22 Sep 2005 23:55:42 +0200 |
nipkow |
fix because of list lemmas
|
changeset |
files
|
| Thu, 22 Sep 2005 23:43:55 +0200 |
nipkow |
renamed "rules" to "iprover"
|
changeset |
files
|
| Thu, 22 Sep 2005 19:06:34 +0200 |
huffman |
added theorem adm_ball
|
changeset |
files
|
| Thu, 22 Sep 2005 19:06:05 +0200 |
huffman |
cleaned up
|
changeset |
files
|
| Thu, 22 Sep 2005 18:59:41 +0200 |
huffman |
HOLCF theorem naming conventions
|
changeset |
files
|
| Thu, 22 Sep 2005 14:09:48 +0200 |
paulson |
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
|
changeset |
files
|
| Thu, 22 Sep 2005 14:02:14 +0200 |
nipkow |
Fix because of new lemma in List
|
changeset |
files
|
| Thu, 22 Sep 2005 13:52:55 +0200 |
webertj |
solver "auto" does not reverse the list of solvers anymore
|
changeset |
files
|
| Thu, 22 Sep 2005 07:56:16 +0200 |
haftmann |
added fold_map_graph
|
changeset |
files
|
| Thu, 22 Sep 2005 07:56:04 +0200 |
haftmann |
added fold_map_table
|
changeset |
files
|
| Thu, 22 Sep 2005 00:30:31 +0200 |
isatest |
only show trunk in Changelog (kleing)
|
changeset |
files
|
| Wed, 21 Sep 2005 22:01:09 +0200 |
webertj |
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
|
changeset |
files
|
| Wed, 21 Sep 2005 21:01:27 +0200 |
wenzelm |
echo HOL_USEDIR_OPTIONS;
|
changeset |
files
|
| Wed, 21 Sep 2005 21:00:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 20:26:45 +0200 |
wenzelm |
PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);
|
changeset |
files
|
| Wed, 21 Sep 2005 20:16:35 +0200 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| Wed, 21 Sep 2005 20:16:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 19:16:16 +0200 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| Wed, 21 Sep 2005 19:08:33 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Wed, 21 Sep 2005 18:35:31 +0200 |
paulson |
improved proof parsing
|
changeset |
files
|
| Wed, 21 Sep 2005 18:35:19 +0200 |
paulson |
trying to limit the looping
|
changeset |
files
|
| Wed, 21 Sep 2005 18:06:04 +0200 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| Wed, 21 Sep 2005 18:04:49 +0200 |
wenzelm |
new header syntax;
|
changeset |
files
|
| Wed, 21 Sep 2005 17:25:32 +0200 |
haftmann |
introduces update_warn instead of overwrite_warn
|
changeset |
files
|
| Wed, 21 Sep 2005 17:21:35 +0200 |
haftmann |
added AList.make, eq_fst, apr ...
|
changeset |
files
|
| Wed, 21 Sep 2005 16:37:37 +0200 |
haftmann |
unify dist and main
|
changeset |
files
|
| Wed, 21 Sep 2005 14:46:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 14:45:55 +0200 |
wenzelm |
fixed cvs export;
|
changeset |
files
|
| Wed, 21 Sep 2005 14:23:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 14:05:47 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Wed, 21 Sep 2005 14:03:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 14:02:57 +0200 |
wenzelm |
the_default, the_list;
|
changeset |
files
|
| Wed, 21 Sep 2005 14:00:31 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 21 Sep 2005 14:00:28 +0200 |
wenzelm |
quote "value";
|
changeset |
files
|
| Wed, 21 Sep 2005 13:28:44 +0200 |
wenzelm |
removed "--" argument;
|
changeset |
files
|
| Wed, 21 Sep 2005 13:16:40 +0200 |
wenzelm |
isatool fixheaders;
|
changeset |
files
|
| Wed, 21 Sep 2005 12:03:41 +0200 |
berghofe |
Added new "value" command.
|
changeset |
files
|
| Wed, 21 Sep 2005 12:02:56 +0200 |
berghofe |
Simplified code generator for numerals.
|
changeset |
files
|
| Wed, 21 Sep 2005 12:02:19 +0200 |
berghofe |
Declared nat_number_of as code lemma.
|
changeset |
files
|
| Wed, 21 Sep 2005 12:01:31 +0200 |
berghofe |
- Added eval_term function and value command
|
changeset |
files
|
| Wed, 21 Sep 2005 11:50:52 +0200 |
wenzelm |
tunes;
|
changeset |
files
|
| Wed, 21 Sep 2005 11:50:38 +0200 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| Wed, 21 Sep 2005 11:50:20 +0200 |
wenzelm |
HOL-Complex-Matrix: fixed deps;
|
changeset |
files
|
| Wed, 21 Sep 2005 11:49:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 11:19:16 +0200 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| Wed, 21 Sep 2005 10:40:28 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 10:39:38 +0200 |
haftmann |
(name mess cleanup)
|
changeset |
files
|
| Wed, 21 Sep 2005 10:33:59 +0200 |
haftmann |
introduced AList module
|
changeset |
files
|
| Wed, 21 Sep 2005 10:32:24 +0200 |
haftmann |
removed assoc, overwrite
|
changeset |
files
|
| Wed, 21 Sep 2005 10:32:06 +0200 |
haftmann |
added update_warn
|
changeset |
files
|
| Wed, 21 Sep 2005 00:07:32 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Sep 2005 23:36:57 +0200 |
wenzelm |
fixed proof script of lemma merges_same_conv (Why did it stop working?);
|
changeset |
files
|
| Tue, 20 Sep 2005 22:07:36 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 20 Sep 2005 22:02:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Sep 2005 21:51:06 +0200 |
wenzelm |
HOL/ex/Chinese.thy;
|
changeset |
files
|
| Tue, 20 Sep 2005 21:48:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Sep 2005 21:48:37 +0200 |
wenzelm |
more contributions;
|
changeset |
files
|
| Tue, 20 Sep 2005 21:39:00 +0200 |
wenzelm |
tuned headers;
|
changeset |
files
|
| Tue, 20 Sep 2005 21:34:20 +0200 |
wenzelm |
tuned header;
|
changeset |
files
|
| Tue, 20 Sep 2005 21:09:41 +0200 |
wenzelm |
use "ML-Systems/smlnj-basis-compat.ML" *after* Interrupt;
|
changeset |
files
|
| Tue, 20 Sep 2005 20:16:55 +0200 |
wenzelm |
fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
|
changeset |
files
|
| Tue, 20 Sep 2005 19:38:35 +0200 |
webertj |
bugfix in "zchaff_with_proofs"
|
changeset |
files
|
| Tue, 20 Sep 2005 18:47:42 +0200 |
paulson |
fixed recursive-looking declaration
|
changeset |
files
|
| Tue, 20 Sep 2005 18:43:39 +0200 |
paulson |
tidying, and support for axclass/classrel clauses
|
changeset |
files
|
| Tue, 20 Sep 2005 18:42:56 +0200 |
paulson |
fixed syntax for sml/nj
|
changeset |
files
|
| Tue, 20 Sep 2005 17:01:43 +0200 |
webertj |
undone the previous change: show_hyps not supported anymore
|
changeset |
files
|
| Tue, 20 Sep 2005 16:19:51 +0200 |
webertj |
pointers to src/HOL/Tools/sat_solver.ML added in comments
|
changeset |
files
|
| Tue, 20 Sep 2005 16:17:34 +0200 |
haftmann |
introduced AList module in favor of assoc etc.
|
changeset |
files
|
| Tue, 20 Sep 2005 15:12:40 +0200 |
webertj |
new menu item show-sort-hypotheses to toggle show_hyps
|
changeset |
files
|
| Tue, 20 Sep 2005 14:20:58 +0200 |
wenzelm |
HOL/ex/Chinese.thy;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:17:31 +0200 |
wenzelm |
HOL-ex: Library/Commutative_Ring.thy;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:13:20 +0200 |
wenzelm |
moved Tools/comm_ring.ML to Library;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:10:29 +0200 |
wenzelm |
added Commutative_Ring (from Main HOL);
|
changeset |
files
|
| Tue, 20 Sep 2005 14:06:00 +0200 |
wenzelm |
Simplifier.inherit_bounds;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:04:34 +0200 |
wenzelm |
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:03:42 +0200 |
wenzelm |
get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:03:41 +0200 |
wenzelm |
removed obsolete thms_containing;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:03:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:03:39 +0200 |
wenzelm |
tuned simprocs;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:03:38 +0200 |
wenzelm |
removed Commutative_Ring hacks;
|
changeset |
files
|
| Tue, 20 Sep 2005 14:03:37 +0200 |
wenzelm |
tuned theory dependencies;
|
changeset |
files
|
| Tue, 20 Sep 2005 13:58:58 +0200 |
wenzelm |
removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
|
changeset |
files
|
| Tue, 20 Sep 2005 13:57:08 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Sep 2005 13:56:34 +0200 |
wenzelm |
Chinese Unicode example;
|
changeset |
files
|
| Tue, 20 Sep 2005 13:56:01 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 20 Sep 2005 13:33:27 +0200 |
chaieb |
The simpset of the actual theory is take, in order to handle rings defined after the method
|
changeset |
files
|
| Tue, 20 Sep 2005 13:17:55 +0200 |
paulson |
further tidying; killing of old Watcher loops
|
changeset |
files
|
| Tue, 20 Sep 2005 13:17:55 +0200 |
nipkow |
added a number of lemmas
|
changeset |
files
|
| Tue, 20 Sep 2005 13:17:32 +0200 |
paulson |
uniform handling of interrupts
|
changeset |
files
|
| Tue, 20 Sep 2005 10:36:33 +0200 |
chaieb |
algebra method added.
|
changeset |
files
|
| Tue, 20 Sep 2005 08:24:18 +0200 |
haftmann |
improved eq_fst and eq_snd, removed some deprecated stuff
|
changeset |
files
|
| Tue, 20 Sep 2005 08:23:59 +0200 |
haftmann |
added make and find
|
changeset |
files
|
| Tue, 20 Sep 2005 08:21:49 +0200 |
haftmann |
slight adaptions to library changes
|
changeset |
files
|
| Tue, 20 Sep 2005 08:20:22 +0200 |
haftmann |
infix operator precedence
|
changeset |
files
|
| Tue, 20 Sep 2005 00:16:29 +0200 |
webertj |
using curried Inttab.update_new function now
|
changeset |
files
|
| Mon, 19 Sep 2005 23:45:59 +0200 |
webertj |
SAT solver interface modified to support proofs of unsatisfiability
|
changeset |
files
|
| Mon, 19 Sep 2005 23:23:51 +0200 |
wenzelm |
shrink: compress terms and types;
|
changeset |
files
|
| Mon, 19 Sep 2005 23:22:51 +0200 |
wenzelm |
added String.isSuffix;
|
changeset |
files
|
| Mon, 19 Sep 2005 22:35:39 +0200 |
obua |
maybe the last bug fix (sigh)?
|
changeset |
files
|
| Mon, 19 Sep 2005 19:49:09 +0200 |
obua |
Removed superfluous HOL/Matrix/cplex/ROOT.ML.
|
changeset |
files
|
| Mon, 19 Sep 2005 18:30:22 +0200 |
paulson |
further simplification of the Isabelle-ATP linkup
|
changeset |
files
|
| Mon, 19 Sep 2005 16:42:11 +0200 |
haftmann |
added make function
|
changeset |
files
|
| Mon, 19 Sep 2005 16:39:27 +0200 |
haftmann |
removed some deprecated assocation list functions
|
changeset |
files
|
| Mon, 19 Sep 2005 16:38:35 +0200 |
haftmann |
introduced AList module
|
changeset |
files
|
| Mon, 19 Sep 2005 15:12:13 +0200 |
paulson |
simplification of the Isabelle-ATP code; hooks for batch generation of problems
|
changeset |
files
|
| Mon, 19 Sep 2005 14:20:45 +0200 |
kleing |
update usage message
|
changeset |
files
|
| Mon, 19 Sep 2005 12:05:08 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sun, 18 Sep 2005 15:20:08 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sun, 18 Sep 2005 14:25:48 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sat, 17 Sep 2005 20:49:14 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sat, 17 Sep 2005 20:16:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 17 Sep 2005 20:14:30 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sat, 17 Sep 2005 19:17:35 +0200 |
wenzelm |
moved quick_and_dirty to Pure/ROOT.ML;
|
changeset |
files
|
| Sat, 17 Sep 2005 19:17:34 +0200 |
wenzelm |
pretty_thm_aux: ora masked by quick_and_dirty;
|
changeset |
files
|
| Sat, 17 Sep 2005 19:17:33 +0200 |
wenzelm |
added quick_and_dirty (from Isar/skip_proofs.ML);
|
changeset |
files
|
| Sat, 17 Sep 2005 19:12:58 +0200 |
wenzelm |
manually generated from Isabelle/HOLCF/IOA/Complex/Import;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:25:11 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:24:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:30 +0200 |
wenzelm |
added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:29 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:28 +0200 |
wenzelm |
pretty_thm_aux: aconv hyps;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:27 +0200 |
wenzelm |
removed obsolete BasisLibrary;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:26 +0200 |
wenzelm |
Hebrew: HTML.with_charset;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:25 +0200 |
wenzelm |
removed obsolete BasisLibrary;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:24 +0200 |
wenzelm |
added quickcheck_params (from Main.thy);
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:23 +0200 |
wenzelm |
removed spurious PolyML.exception_trace;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:22 +0200 |
wenzelm |
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:21 +0200 |
wenzelm |
minor cleanup, moved stuff in its proper place;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:20 +0200 |
wenzelm |
generate: added HOL-Complex-Generate-HOLLight;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:19 +0200 |
wenzelm |
added code generator setup (from Main.thy);
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:18 +0200 |
wenzelm |
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:17 +0200 |
wenzelm |
HTML.with_charset;
|
changeset |
files
|
| Sat, 17 Sep 2005 17:35:26 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sat, 17 Sep 2005 14:02:31 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:51:03 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:50:57 +0200 |
wenzelm |
plain test session, includes example;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:08 +0200 |
wenzelm |
theory_to_proof: check theory of initial proof state, which must not be changed;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:07 +0200 |
wenzelm |
added auto_fix (from proof.ML);
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:06 +0200 |
wenzelm |
export put_facts;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:05 +0200 |
wenzelm |
interpretation: use goal commands without target -- no storing of results;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:04 +0200 |
wenzelm |
theorem(_i): empty target;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:03 +0200 |
wenzelm |
pretty_thm_aux: observe asms context;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:00 +0200 |
wenzelm |
Cube: converted to Isar, use locales;
|
changeset |
files
|
| Sat, 17 Sep 2005 11:49:29 +0200 |
obua |
1) mapped .. and == constants
|
changeset |
files
|
| Sat, 17 Sep 2005 01:50:01 +0200 |
huffman |
use interpretation command
|
changeset |
files
|
| Fri, 16 Sep 2005 23:55:23 +0200 |
huffman |
add HOLCF entries for pcpodef, cont_proc, fixrec;
|
changeset |
files
|
| Fri, 16 Sep 2005 23:01:29 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Fri, 16 Sep 2005 21:02:15 +0200 |
obua |
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
|
changeset |
files
|
| Fri, 16 Sep 2005 20:30:44 +0200 |
huffman |
add header
|
changeset |
files
|
| Fri, 16 Sep 2005 16:07:22 +0200 |
ballarin |
tuned
|
changeset |
files
|
| Fri, 16 Sep 2005 14:46:31 +0200 |
ballarin |
interpretation uses primitive goal interface
|
changeset |
files
|
| Fri, 16 Sep 2005 14:44:52 +0200 |
ballarin |
tuned
|
changeset |
files
|
| Fri, 16 Sep 2005 11:39:09 +0200 |
paulson |
PARTIAL conversion to Vampire8
|
changeset |
files
|
| Fri, 16 Sep 2005 11:38:49 +0200 |
paulson |
catching exception Io
|
changeset |
files
|
| Fri, 16 Sep 2005 02:20:50 +0200 |
huffman |
rearranged
|
changeset |
files
|
| Fri, 16 Sep 2005 01:42:57 +0200 |
huffman |
use mem operator
|
changeset |
files
|
| Fri, 16 Sep 2005 01:34:53 +0200 |
huffman |
fix names in hypreal_arith.ML
|
changeset |
files
|
| Thu, 15 Sep 2005 23:53:33 +0200 |
huffman |
merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
|
changeset |
files
|
| Thu, 15 Sep 2005 23:46:22 +0200 |
huffman |
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
|
changeset |
files
|
| Thu, 15 Sep 2005 23:16:04 +0200 |
huffman |
add header
|
changeset |
files
|
| Thu, 15 Sep 2005 22:16:23 +0200 |
chaieb |
The SMLNJ Problem fixed...
|
changeset |
files
|
| Thu, 15 Sep 2005 20:38:47 +0200 |
chaieb |
getting it work for SMLNJ
|
changeset |
files
|
| Thu, 15 Sep 2005 20:27:48 +0200 |
wenzelm |
* Improved efficiency of the Simplifier etc.;
|
changeset |
files
|
| Thu, 15 Sep 2005 20:25:04 +0200 |
wenzelm |
incorporated into NEWS;
|
changeset |
files
|
| Thu, 15 Sep 2005 20:24:53 +0200 |
wenzelm |
incorporated HOL/Hyperreal/CHANGES;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:46:00 +0200 |
paulson |
massive tidy-up and simplification
|
changeset |
files
|
| Thu, 15 Sep 2005 17:45:17 +0200 |
paulson |
moving Commutative_Ring to the correct theory
|
changeset |
files
|
| Thu, 15 Sep 2005 17:44:53 +0200 |
paulson |
comment
|
changeset |
files
|
| Thu, 15 Sep 2005 17:18:57 +0200 |
wenzelm |
poly -doDisplay;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:17:06 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:17:05 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:17:04 +0200 |
wenzelm |
fixed type;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:17:03 +0200 |
wenzelm |
fixed ML;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:17:02 +0200 |
wenzelm |
The Hebrew Alef-Bet -- Unicode example;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:17:01 +0200 |
wenzelm |
added Hebrew.thy;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:16:55 +0200 |
wenzelm |
fixed document;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:16:54 +0200 |
wenzelm |
added HOL/ex/Hebrew.thy;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:16:53 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Thu, 15 Sep 2005 17:16:53 +0200 |
wenzelm |
command 'thms_containing' has been discontinued in favour of 'find_theorems';
|
changeset |
files
|
| Thu, 15 Sep 2005 16:15:22 +0200 |
aspinall |
Revert previous attribute name change, problem can be avoided in JAXB.
|
changeset |
files
|
| Thu, 15 Sep 2005 13:36:10 +0200 |
wenzelm |
forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;
|
changeset |
files
|
| Thu, 15 Sep 2005 13:35:21 +0200 |
wenzelm |
extend: NameSpace.default_naming;
|
changeset |
files
|
| Thu, 15 Sep 2005 11:15:52 +0200 |
paulson |
the experimental tagging system, and the usual tidying
|
changeset |
files
|
| Thu, 15 Sep 2005 10:33:35 +0200 |
aspinall |
Change PGIP attribute name class->messageclass to avoid Java keyword clash.
|
changeset |
files
|
| Thu, 15 Sep 2005 10:00:01 +0200 |
haftmann |
AList, the_*
|
changeset |
files
|
| Thu, 15 Sep 2005 08:16:22 +0200 |
haftmann |
fixed type annotation
|
changeset |
files
|
| Thu, 15 Sep 2005 07:35:38 +0200 |
haftmann |
added gen_list to Pretty module
|
changeset |
files
|
| Wed, 14 Sep 2005 23:55:49 +0200 |
wenzelm |
@{term [source] ...} in subsections probably more robust;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:31:09 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:15:00 +0200 |
wenzelm |
hide: added option '(open)';
|
changeset |
files
|
| Wed, 14 Sep 2005 23:14:59 +0200 |
wenzelm |
imports Commutative_Ring instead of Main, since the latter hides our names;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:14:58 +0200 |
wenzelm |
hide the rather generic names used in theory Commutative_Ring;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:14:57 +0200 |
wenzelm |
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:06:02 +0200 |
schirmer |
... prem19
|
changeset |
files
|
| Wed, 14 Sep 2005 23:04:59 +0200 |
schirmer |
added prem10 - prem19
|
changeset |
files
|
| Wed, 14 Sep 2005 23:03:52 +0200 |
schirmer |
removed syntax fun_map_comp;
|
changeset |
files
|
| Wed, 14 Sep 2005 23:00:03 +0200 |
chaieb |
Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
|
changeset |
files
|
| Wed, 14 Sep 2005 22:18:55 +0200 |
wenzelm |
Method comm_ring for proving equalities in commutative rings.
|
changeset |
files
|
| Wed, 14 Sep 2005 22:08:08 +0200 |
wenzelm |
tuned headers etc.;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:38 +0200 |
wenzelm |
fixed some ML names;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:37 +0200 |
wenzelm |
imports Commutative_Ring;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:36 +0200 |
wenzelm |
HOL: method comm_ring;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:34 +0200 |
wenzelm |
no longer prefer xemacs, which fails more often than GNU emacs;
|
changeset |
files
|
| Wed, 14 Sep 2005 22:04:33 +0200 |
wenzelm |
Bernhard Haeupler: comm_ring;
|
changeset |
files
|
| Wed, 14 Sep 2005 21:44:27 +0200 |
chaieb |
tactic and the rest eliminated, just the theory....
|
changeset |
files
|
| Wed, 14 Sep 2005 21:35:46 +0200 |
chaieb |
use was wrong...
|
changeset |
files
|
| Wed, 14 Sep 2005 19:03:16 +0200 |
obua |
Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
|
changeset |
files
|
| Wed, 14 Sep 2005 17:25:52 +0200 |
chaieb |
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
|
changeset |
files
|
| Wed, 14 Sep 2005 10:24:39 +0200 |
haftmann |
introduced AList.lookup
|
changeset |
files
|
| Wed, 14 Sep 2005 10:21:09 +0200 |
paulson |
correct E brackets
|
changeset |
files
|
| Wed, 14 Sep 2005 10:20:50 +0200 |
paulson |
nice names for more infix operators
|
changeset |
files
|
| Wed, 14 Sep 2005 10:13:12 +0200 |
haftmann |
introduces AList.lookup
|
changeset |
files
|
| Wed, 14 Sep 2005 01:47:06 +0200 |
huffman |
removed duplicated lemmas; convert more proofs to transfer principle
|
changeset |
files
|
| Tue, 13 Sep 2005 23:30:01 +0200 |
huffman |
add theorem chain_const
|
changeset |
files
|
| Tue, 13 Sep 2005 22:49:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:21:06 +0200 |
wenzelm |
global quick_and_dirty;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:54 +0200 |
wenzelm |
Printing of Isar proof elements etc.
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:53 +0200 |
wenzelm |
Non-empty stacks.
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:52 +0200 |
wenzelm |
IsarThy.begin_theory;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:51 +0200 |
wenzelm |
export ml_exts;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:50 +0200 |
wenzelm |
begin_theory: tuned interface, check uses;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:49 +0200 |
wenzelm |
replaced TRANSLATION_FAIL by EXCEPTION;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:48 +0200 |
wenzelm |
added three_buffersN, print3;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:47 +0200 |
wenzelm |
load before proof.ML;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:46 +0200 |
wenzelm |
added simple;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:45 +0200 |
wenzelm |
added add_view, export_view (supercedes adhoc view arguments);
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:44 +0200 |
wenzelm |
major cleanup of interfaces and implementation;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:43 +0200 |
wenzelm |
added name_facts;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:42 +0200 |
wenzelm |
tuned Isar proof elements;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:40 +0200 |
wenzelm |
added cheating, sorry_text (from skip_proofs.ML);
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:39 +0200 |
wenzelm |
load late, after proof.ML;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:38 +0200 |
wenzelm |
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:37 +0200 |
wenzelm |
cleanup parsers and interfaces;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:36 +0200 |
wenzelm |
Proof.get_thmss;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:34 +0200 |
wenzelm |
more self-contained proof elements (material from isar_thy.ML);
|
changeset |
files
|
| Tue, 13 Sep 2005 22:19:33 +0200 |
wenzelm |
added cases, rule_contextN;
|
changeset |
files
|