| 1999-05-24 |
paulson |
now uses mono_Increasing_o
|
changeset |
files
|
| 1999-05-24 |
paulson |
updated for stronger version of psp
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
Configuration for ProofGeneral of LFCS Edinburgh.
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
Configuration for David Aspinall's Isamode.
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
Miscellaneous interfaces.
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
Isamode.setup, ProofGeneral.setup;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
Isamode and ProofGeneral configuration moved to Pure/Interface;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
added use_thy_only;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
avoid string constants;
|
changeset |
files
|
| 1999-05-21 |
nipkow |
qed indexed.
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
typedef_proof: pass interactive flag;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
tuned;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
cleaned comments;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
renamed 'begin' / 'end' to '{{' / '}}';
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
history commands;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
tuned;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
adapted to History changes;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
local_qed: obtain interactive flag;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
backup replaced by checkpoint;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
added default_prompt;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
optional limit;
|
changeset |
files
|
| 1999-05-21 |
wenzelm |
improved errors;
|
changeset |
files
|
| 1999-05-21 |
paulson |
updated comment
|
changeset |
files
|
| 1999-05-21 |
paulson |
made definition more readable
|
changeset |
files
|
| 1999-05-21 |
paulson |
preferring generic rules to specific ones...
|
changeset |
files
|
| 1999-05-21 |
paulson |
changes to show that Lists are partially ordered by the prefix relation
|
changeset |
files
|
| 1999-05-21 |
paulson |
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)
|
changeset |
files
|
| 1999-05-19 |
paulson |
redid proofs to use "always" rather than "reachable" (somewhat)
|
changeset |
files
|
| 1999-05-19 |
paulson |
new theorem Always_reachable
|
changeset |
files
|
| 1999-05-18 |
wenzelm |
tuned;
|
changeset |
files
|
| 1999-05-18 |
paulson |
added Locale paper
|
changeset |
files
|
| 1999-05-18 |
paulson |
locale documentation (from Florian)
|
changeset |
files
|
| 1999-05-18 |
paulson |
../manual.bib a new dependency
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
cleaned comments;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
cleaned comments;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
tuned;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
cleaned comments;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
ThyInfo.finalize_all renamed to ThyInfo.finish;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
node_cases renamed to node_case;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
prep_ext exported (again);
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
backup operation replaces transaction;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
removed get_nodes;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
remove_thy;
|
changeset |
files
|
| 1999-05-17 |
wenzelm |
tuned arrows;
|
changeset |
files
|
| 1999-05-17 |
berghofe |
Arrows are no longer needed because of redesign of the
|
changeset |
files
|
| 1999-05-17 |
berghofe |
Changed some file names.
|
changeset |
files
|
| 1999-05-17 |
berghofe |
Added function get_preds.
|
changeset |
files
|
| 1999-05-17 |
berghofe |
Added setup for BrowserInfo.
|
changeset |
files
|
| 1999-05-17 |
berghofe |
usedir now recognizes additional option -P which is used to
|
changeset |
files
|
| 1999-05-17 |
berghofe |
Changed interface of function use_dir.
|
changeset |
files
|
| 1999-05-17 |
berghofe |
Present.begin_theory now needs an additional argument of type
|
changeset |
files
|
| 1999-05-17 |
berghofe |
Reimplemented graph generator.
|
changeset |
files
|
| 1999-05-17 |
berghofe |
Added some code to enable browser to display remote documents.
|
changeset |
files
|
| 1999-05-17 |
paulson |
new thm extend_JN; renamed extend_leadsto
|
changeset |
files
|
| 1999-05-17 |
paulson |
"component" now an infix
|
changeset |
files
|
| 1999-05-17 |
paulson |
indentation
|
changeset |
files
|
| 1999-05-15 |
wenzelm |
tuned;
|
changeset |
files
|
| 1999-05-12 |
wenzelm |
ad-hoc fix for bold indexes;
|
changeset |
files
|
| 1999-05-12 |
wenzelm |
strip_quotes replaced by unenclose;
|
changeset |
files
|