| Tue, 09 Jan 2007 15:49:39 +0100 |
paulson |
simplified the resoution proofs
|
changeset |
files
|
| Tue, 09 Jan 2007 12:12:00 +0100 |
aspinall |
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
|
changeset |
files
|
| Tue, 09 Jan 2007 12:09:49 +0100 |
aspinall |
Add info fatality for error messages.
|
changeset |
files
|
| Tue, 09 Jan 2007 12:09:21 +0100 |
aspinall |
Add informfileoutdated and completed flag. This makes the PGIP messages match the Broker states.
|
changeset |
files
|
| Tue, 09 Jan 2007 08:32:50 +0100 |
haftmann |
slight cleanups
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:54 +0100 |
haftmann |
improved names
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:52 +0100 |
haftmann |
proper node names
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:51 +0100 |
haftmann |
slight cleanup
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:50 +0100 |
haftmann |
improved variable name handling
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:49 +0100 |
haftmann |
moved variable environments here
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:48 +0100 |
haftmann |
moved a lot to codegen_func.ML
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:47 +0100 |
haftmann |
typo
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:46 +0100 |
haftmann |
added map_abs_vars
|
changeset |
files
|
| Mon, 08 Jan 2007 12:26:13 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 07 Jan 2007 16:21:22 +0100 |
webertj |
print functions for typs and terms added
|
changeset |
files
|
| Sun, 07 Jan 2007 14:05:44 +0100 |
aspinall |
Be more chatty in PGIP file operations.
|
changeset |
files
|
| Sat, 06 Jan 2007 20:56:44 +0100 |
chaieb |
A few lemmas about relative primes when dividing trough gcd
|
changeset |
files
|
| Sat, 06 Jan 2007 20:47:09 +0100 |
chaieb |
A few theorems on integer divisibily.
|
changeset |
files
|
| Fri, 05 Jan 2007 17:38:05 +0100 |
paulson |
Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever
|
changeset |
files
|
| Fri, 05 Jan 2007 15:33:05 +0100 |
webertj |
reverted to v1.60 (PolyML 4.1.3 still has the wrong signature for Array.modifyi)
|
changeset |
files
|
| Fri, 05 Jan 2007 14:32:07 +0100 |
haftmann |
added codegen_func.ML
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:51 +0100 |
haftmann |
non-layout-sensitive syntax for Haskell
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:50 +0100 |
haftmann |
some cleanup
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:49 +0100 |
haftmann |
primitive definitions are always eta-expanded
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:48 +0100 |
haftmann |
added block_enclose
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:47 +0100 |
haftmann |
added CodeEval
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:46 +0100 |
haftmann |
dealing with ml_string and char instances
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:45 +0100 |
haftmann |
dealing with ml_string combinators
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:44 +0100 |
haftmann |
adaptions
|
changeset |
files
|
| Fri, 05 Jan 2007 14:30:08 +0100 |
wenzelm |
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
|
changeset |
files
|
| Fri, 05 Jan 2007 14:30:07 +0100 |
wenzelm |
RAW-ProofGeneral: more dependencies;
|
changeset |
files
|
| Fri, 05 Jan 2007 13:36:32 +0100 |
paulson |
Proof.context now sent to watcher and used in type inference step of proof reconstruction
|
changeset |
files
|
| Thu, 04 Jan 2007 21:58:46 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Thu, 04 Jan 2007 21:37:02 +0100 |
wenzelm |
removed obsolete ProofGeneral/syntax_standalone.ML;
|
changeset |
files
|
| Thu, 04 Jan 2007 21:36:52 +0100 |
wenzelm |
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
|
changeset |
files
|
| Thu, 04 Jan 2007 21:18:05 +0100 |
wenzelm |
added mk_simproc': tuned interface;
|
changeset |
files
|
| Thu, 04 Jan 2007 20:01:02 +0100 |
haftmann |
clarification
|
changeset |
files
|
| Thu, 04 Jan 2007 20:01:01 +0100 |
haftmann |
dropped function theorems are considered as deleted
|
changeset |
files
|
| Thu, 04 Jan 2007 20:01:00 +0100 |
haftmann |
examples for evaluation oracle
|
changeset |
files
|
| Thu, 04 Jan 2007 20:00:59 +0100 |
haftmann |
fixed eval oracle
|
changeset |
files
|
| Thu, 04 Jan 2007 19:53:00 +0100 |
aspinall |
Be more chatty in PGIP file operations.proof_general_pgip.ML
|
changeset |
files
|
| Thu, 04 Jan 2007 19:27:08 +0100 |
wenzelm |
broken error handling for command syntax -- reverted to revision 1.9;
|
changeset |
files
|
| Thu, 04 Jan 2007 18:09:58 +0100 |
aspinall |
Use warning fatality
|
changeset |
files
|
| Thu, 04 Jan 2007 18:09:30 +0100 |
aspinall |
Add warning fatality
|
changeset |
files
|
| Thu, 04 Jan 2007 17:55:12 +0100 |
paulson |
improvements to proof reconstruction. Some files loaded in a different order
|
changeset |
files
|
| Thu, 04 Jan 2007 17:52:28 +0100 |
webertj |
using Array.modifyi (no functional change)
|
changeset |
files
|
| Thu, 04 Jan 2007 17:49:43 +0100 |
wenzelm |
run as RAW session;
|
changeset |
files
|
| Thu, 04 Jan 2007 17:49:42 +0100 |
wenzelm |
removed obsolete option -C;
|
changeset |
files
|
| Thu, 04 Jan 2007 17:49:41 +0100 |
wenzelm |
removed obsolete Pure-copied target;
|
changeset |
files
|
| Thu, 04 Jan 2007 17:17:48 +0100 |
haftmann |
updated manual
|
changeset |
files
|
| Thu, 04 Jan 2007 17:11:09 +0100 |
haftmann |
updated manual
|
changeset |
files
|
| Thu, 04 Jan 2007 15:29:44 +0100 |
webertj |
obsolete sign_of calls removed
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:41 +0100 |
haftmann |
fixed output
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:40 +0100 |
haftmann |
different handling of eta expansion
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:39 +0100 |
haftmann |
eta-expansion now only to common maximum number of arguments
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:38 +0100 |
haftmann |
clarified code
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:37 +0100 |
haftmann |
more term examples
|
changeset |
files
|
| Thu, 04 Jan 2007 11:56:53 +0100 |
haftmann |
eliminated Option.app
|
changeset |
files
|
| Thu, 04 Jan 2007 00:12:30 +0100 |
webertj |
constants are unfolded, universal quantifiers are stripped, some minor changes
|
changeset |
files
|
| Wed, 03 Jan 2007 22:59:30 +0100 |
aspinall |
Fix error reporting in Emacs to also match Isar command failure exactly.
|
changeset |
files
|
| Wed, 03 Jan 2007 21:11:42 +0100 |
aspinall |
Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
|
changeset |
files
|
| Wed, 03 Jan 2007 21:09:13 +0100 |
aspinall |
Expose command failure recovery code for top level.
|
changeset |
files
|
| Wed, 03 Jan 2007 21:00:24 +0100 |
aspinall |
Selected functions from syntax module
|
changeset |
files
|
| Wed, 03 Jan 2007 18:30:57 +0100 |
paulson |
x-symbol is no longer switched off in the ATP linkup
|
changeset |
files
|
| Wed, 03 Jan 2007 18:29:46 +0100 |
paulson |
Improvements to proof reconstruction. Now "fixes" is inserted
|
changeset |
files
|
| Wed, 03 Jan 2007 11:06:52 +0100 |
paulson |
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
|
changeset |
files
|
| Wed, 03 Jan 2007 10:59:06 +0100 |
paulson |
first version of structured proof reconstruction
|
changeset |
files
|
| Tue, 02 Jan 2007 22:43:05 +0100 |
wenzelm |
Morphism.fact;
|
changeset |
files
|
| Tue, 02 Jan 2007 22:43:04 +0100 |
wenzelm |
Term.lambda: abstract over arbitrary closed terms;
|
changeset |
files
|
| Sun, 31 Dec 2006 15:57:58 +0100 |
aspinall |
Add standalone file to help porters
|
changeset |
files
|
| Sun, 31 Dec 2006 15:34:21 +0100 |
aspinall |
Quote arguments in PGIP exceptions. Tune comment.
|
changeset |
files
|
| Sun, 31 Dec 2006 14:55:35 +0100 |
aspinall |
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
|
changeset |
files
|
| Sun, 31 Dec 2006 14:50:40 +0100 |
aspinall |
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
|
changeset |
files
|
| Sat, 30 Dec 2006 16:20:32 +0100 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:10 +0100 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:09 +0100 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:07 +0100 |
wenzelm |
refrain from setting ml_prompts again;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:06 +0100 |
wenzelm |
removed misleading OuterLex.eq_token;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:05 +0100 |
wenzelm |
pretty_statement: more careful handling of name_hint;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:04 +0100 |
wenzelm |
added has_name_hint;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:03 +0100 |
wenzelm |
removed obsolete name_hint handling;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:41:59 +0100 |
wenzelm |
removed obsolete support for polyml-4.9.1;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:38:51 +0100 |
wenzelm |
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:29 +0100 |
wenzelm |
inform_file_processed: Toplevel.init_empty;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:28 +0100 |
wenzelm |
refined notion of empty toplevel, admits undo of 'end';
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:27 +0100 |
wenzelm |
Toplevel.init_state;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:26 +0100 |
wenzelm |
removed obsolete 'clear_undos';
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:25 +0100 |
wenzelm |
removed obsolete clear_undos_theory;
|
changeset |
files
|
| Fri, 29 Dec 2006 20:35:03 +0100 |
haftmann |
major restructurings
|
changeset |
files
|
| Fri, 29 Dec 2006 20:35:02 +0100 |
haftmann |
cleanup
|
changeset |
files
|
| Fri, 29 Dec 2006 20:34:18 +0100 |
haftmann |
improved print of constructors in OCaml
|
changeset |
files
|
| Fri, 29 Dec 2006 20:34:17 +0100 |
haftmann |
changed syntax for axclass attach
|
changeset |
files
|
| Fri, 29 Dec 2006 19:50:52 +0100 |
wenzelm |
removed obsolete cond_add_path;
|
changeset |
files
|
| Fri, 29 Dec 2006 19:50:51 +0100 |
wenzelm |
removed obsolete context_thy etc.;
|
changeset |
files
|
| Fri, 29 Dec 2006 19:50:50 +0100 |
wenzelm |
removed obsolete init_pgip;
|
changeset |
files
|
| Fri, 29 Dec 2006 19:50:48 +0100 |
wenzelm |
removed obsolete init_context;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:47:11 +0100 |
wenzelm |
obsolete (cf. ProofGeneral/proof_general_emacs.ML);
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:06 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:04 +0100 |
wenzelm |
signed_string_of_int;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:04 +0100 |
wenzelm |
added proper header;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:02 +0100 |
wenzelm |
added signed_string_of_int (pruduces proper - instead of SML's ~);
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:01 +0100 |
wenzelm |
removed obsolete proof_general.ML;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:25:46 +0100 |
wenzelm |
minor tuning;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:25:45 +0100 |
wenzelm |
tuned specifications/proofs;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:49 +0100 |
wenzelm |
replaced Sign.classes by Sign.all_classes (topologically sorted);
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:49 +0100 |
wenzelm |
renamed Graph.project to Graph.subgraph;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:47 +0100 |
wenzelm |
replaced Sign.classes by Sign.all_classes (topologically sorted);
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:46 +0100 |
wenzelm |
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:45 +0100 |
wenzelm |
Sorts.minimal_classes;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:44 +0100 |
wenzelm |
classes: more direct way to achieve topological sorting;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:43 +0100 |
wenzelm |
replaced classes by all_classes (topologically sorted);
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:41 +0100 |
wenzelm |
replaced Sign.classes by Sign.all_classes (topologically sorted);
|
changeset |
files
|
| Fri, 29 Dec 2006 16:47:49 +0100 |
aspinall |
Enable new Proof General code again after SML/NJ compatibility fixes by Florian.
|
changeset |
files
|
| Fri, 29 Dec 2006 16:46:39 +0100 |
aspinall |
Typo in last commit
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:05 +0100 |
haftmann |
explicit construction of operational classes
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:04 +0100 |
haftmann |
added handling for explicit classrel witnesses
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:03 +0100 |
haftmann |
``classes`` now returns classes in topological order
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:02 +0100 |
haftmann |
dropped some bookkeeping
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:00 +0100 |
haftmann |
simplified class_package
|
changeset |
files
|