| 2007-01-04 |
wenzelm |
run as RAW session;
|
changeset |
files
|
| 2007-01-04 |
wenzelm |
removed obsolete option -C;
|
changeset |
files
|
| 2007-01-04 |
wenzelm |
removed obsolete Pure-copied target;
|
changeset |
files
|
| 2007-01-04 |
haftmann |
updated manual
|
changeset |
files
|
| 2007-01-04 |
haftmann |
updated manual
|
changeset |
files
|
| 2007-01-04 |
webertj |
obsolete sign_of calls removed
|
changeset |
files
|
| 2007-01-04 |
haftmann |
fixed output
|
changeset |
files
|
| 2007-01-04 |
haftmann |
different handling of eta expansion
|
changeset |
files
|
| 2007-01-04 |
haftmann |
eta-expansion now only to common maximum number of arguments
|
changeset |
files
|
| 2007-01-04 |
haftmann |
clarified code
|
changeset |
files
|
| 2007-01-04 |
haftmann |
more term examples
|
changeset |
files
|
| 2007-01-04 |
haftmann |
eliminated Option.app
|
changeset |
files
|
| 2007-01-03 |
webertj |
constants are unfolded, universal quantifiers are stripped, some minor changes
|
changeset |
files
|
| 2007-01-03 |
aspinall |
Fix error reporting in Emacs to also match Isar command failure exactly.
|
changeset |
files
|
| 2007-01-03 |
aspinall |
Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
|
changeset |
files
|
| 2007-01-03 |
aspinall |
Expose command failure recovery code for top level.
|
changeset |
files
|
| 2007-01-03 |
aspinall |
Selected functions from syntax module
|
changeset |
files
|
| 2007-01-03 |
paulson |
x-symbol is no longer switched off in the ATP linkup
|
changeset |
files
|
| 2007-01-03 |
paulson |
Improvements to proof reconstruction. Now "fixes" is inserted
|
changeset |
files
|
| 2007-01-03 |
paulson |
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
|
changeset |
files
|
| 2007-01-03 |
paulson |
first version of structured proof reconstruction
|
changeset |
files
|
| 2007-01-02 |
wenzelm |
Morphism.fact;
|
changeset |
files
|
| 2007-01-02 |
wenzelm |
Term.lambda: abstract over arbitrary closed terms;
|
changeset |
files
|
| 2006-12-31 |
aspinall |
Add standalone file to help porters
|
changeset |
files
|
| 2006-12-31 |
aspinall |
Quote arguments in PGIP exceptions. Tune comment.
|
changeset |
files
|
| 2006-12-31 |
aspinall |
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
|
changeset |
files
|
| 2006-12-31 |
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
|
| 2006-12-30 |
wenzelm |
removed dead code;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
refrain from setting ml_prompts again;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
removed misleading OuterLex.eq_token;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
pretty_statement: more careful handling of name_hint;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
added has_name_hint;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
removed obsolete name_hint handling;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
removed obsolete support for polyml-4.9.1;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
inform_file_processed: Toplevel.init_empty;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
refined notion of empty toplevel, admits undo of 'end';
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
Toplevel.init_state;
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
removed obsolete 'clear_undos';
|
changeset |
files
|
| 2006-12-30 |
wenzelm |
removed obsolete clear_undos_theory;
|
changeset |
files
|
| 2006-12-29 |
haftmann |
major restructurings
|
changeset |
files
|
| 2006-12-29 |
haftmann |
cleanup
|
changeset |
files
|
| 2006-12-29 |
haftmann |
improved print of constructors in OCaml
|
changeset |
files
|
| 2006-12-29 |
haftmann |
changed syntax for axclass attach
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
removed obsolete cond_add_path;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
removed obsolete context_thy etc.;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
removed obsolete init_pgip;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
removed obsolete init_context;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
obsolete (cf. ProofGeneral/proof_general_emacs.ML);
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
tuned;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
signed_string_of_int;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
added proper header;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
added signed_string_of_int (pruduces proper - instead of SML's ~);
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
removed obsolete proof_general.ML;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
minor tuning;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
tuned specifications/proofs;
|
changeset |
files
|
| 2006-12-29 |
wenzelm |
replaced Sign.classes by Sign.all_classes (topologically sorted);
|
changeset |
files
|