| 1999-06-05 |
wenzelm |
auto_bind_goal, auto_bind_facts;
|
changeset |
files
|
| 1999-06-05 |
wenzelm |
auto_bind_goal, auto_bind_facts;
|
changeset |
files
|
| 1999-06-05 |
wenzelm |
added get_st;
|
changeset |
files
|
| 1999-06-05 |
wenzelm |
tuned;
|
changeset |
files
|
| 1999-06-05 |
wenzelm |
varifyT': observe additional 'fixed' tfrees;
|
changeset |
files
|
| 1999-06-05 |
wenzelm |
removed ObjectLogic.setup;
|
changeset |
files
|
| 1999-06-05 |
wenzelm |
proper calculation;
|
changeset |
files
|
| 1999-06-05 |
wenzelm |
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
fixed "...": dest_arg;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
oops;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added order_le_less_trans, order_less_le_trans;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
Calculation.thy: Setup transitivity rules for calculational proofs.
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
Support for calculational proofs.
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added put_st;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added the_fact, level;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
export multi_resolve;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added also, finally;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added 'also', 'finally' commands;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added COMP attribute;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added calculation.ML;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added Isar/calculation.ML;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
fixed BUG in have_thmss: return thy';
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added dest_main_statement;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
print "..." variable;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
no message "Adding axioms for datatype(s)";
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added Group.thy;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
added Isar_examples/Group.thy;
|
changeset |
files
|
| 1999-06-04 |
wenzelm |
Some bits of group theory. Demonstrate calculational proofs.
|
changeset |
files
|
| 1999-06-02 |
wenzelm |
read_term/prop_pat: do not freeze;
|
changeset |
files
|
| 1999-06-02 |
wenzelm |
added dddot_tr;
|
changeset |
files
|
| 1999-06-02 |
wenzelm |
added dddot_indexname;
|
changeset |
files
|
| 1999-06-02 |
wenzelm |
"..." syntax;
|
changeset |
files
|
| 1999-06-02 |
wenzelm |
find -print;
|
changeset |
files
|
| 1999-06-01 |
wenzelm |
'kill' made improper;
|
changeset |
files
|
| 1999-06-01 |
wenzelm |
improved print_state;
|
changeset |
files
|
| 1999-06-01 |
wenzelm |
'note': Toplevel.print;
|
changeset |
files
|
| 1999-06-01 |
wenzelm |
tuned markup;
|
changeset |
files
|
| 1999-06-01 |
wenzelm |
broder size 3;
|
changeset |
files
|
| 1999-05-31 |
wenzelm |
setup_goal: proper handling of non-atomic goals (include cprems into asms);
|
changeset |
files
|
| 1999-05-31 |
wenzelm |
Isabelle manuals now also available as PDF;
|
changeset |
files
|
| 1999-05-28 |
wenzelm |
move pdfs back into dist;
|
changeset |
files
|
| 1999-05-28 |
wenzelm |
pdf docs;
|
changeset |
files
|
| 1999-05-28 |
wenzelm |
separate archive for pdf docs;
|
changeset |
files
|
| 1999-05-28 |
wenzelm |
\def\bold;
|
changeset |
files
|
| 1999-05-28 |
wenzelm |
tuned formal comments;
|
changeset |
files
|
| 1999-05-28 |
wenzelm |
tuned manual.bib;
|
changeset |
files
|
| 1999-05-27 |
wenzelm |
changed {| |} verbatim syntax to {* *};
|
changeset |
files
|
| 1999-05-27 |
wenzelm |
changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;
|
changeset |
files
|
| 1999-05-27 |
wenzelm |
improved undo / kill operations;
|
changeset |
files
|
| 1999-05-27 |
paulson |
fixed corruptoin of end of file
|
changeset |
files
|
| 1999-05-27 |
paulson |
removal of Always_StableI
|
changeset |
files
|
| 1999-05-27 |
paulson |
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
|
changeset |
files
|
| 1999-05-27 |
paulson |
component_eq_subset: a neat characterization of "component"
|
changeset |
files
|
| 1999-05-26 |
wenzelm |
ex/Points Isar'ized;
|
changeset |
files
|
| 1999-05-26 |
wenzelm |
local_qed: print_result;
|
changeset |
files
|
| 1999-05-26 |
wenzelm |
cannot_undo;
|
changeset |
files
|
| 1999-05-26 |
wenzelm |
cannot_undo;
|
changeset |
files
|
| 1999-05-26 |
wenzelm |
qed_block keywords;
|
changeset |
files
|
| 1999-05-26 |
wenzelm |
local qeds: pass cond_print_result;
|
changeset |
files
|
| 1999-05-26 |
wenzelm |
cleaned comments;
|
changeset |
files
|