Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-1000
-384
+384
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
Made troublesome simplifier warning dependent on trace_simp.
1997-02-14, by nipkow
Modified and shortened adm_disj lemmas.
1997-02-14, by nipkow
Deleted a useless definition
1997-02-14, by paulson
Added optimization: do nothing for empty list
1997-02-14, by paulson
A bit more pattern-matching in eta_contract
1997-02-14, by paulson
Tidying and a corrected comment
1997-02-14, by paulson
Added a new challenge problem
1997-02-14, by paulson
Updated documentation of IFOL_ss
1997-02-14, by paulson
Documented thin_tac
1997-02-14, by paulson
Strengthened warnings concerning topthm(), etc.
1997-02-14, by paulson
Updated a reference
1997-02-14, by paulson
New class "order" and accompanying changes.
1997-02-12, by nipkow
New class "order" and accompanying changes.
1997-02-12, by nipkow
TFL: missing -q option!
1997-02-12, by wenzelm
tuned names: partial order, linear order;
1997-02-12, by wenzelm
tuned startup;
1997-02-10, by wenzelm
fixed comment;
1997-02-10, by wenzelm
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
1997-02-10, by paulson
Renamed structure Int (intuitionistic prover) to IntPr
1997-02-10, by paulson
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
1997-02-10, by paulson
removed ISABELLE_INTERFACE_OPTIONS;
1997-02-07, by wenzelm
tuned;
1997-02-07, by wenzelm
tuned;
1997-02-07, by wenzelm
Modified proofs due to added triv_forall_equality.
1997-02-07, by nipkow
Modified proofs because of added "triv_forall_equality".
1997-02-07, by nipkow
Added "triv_forall_equality" to HOL_ss.
1997-02-07, by nipkow
functionality added to getsettings;
1997-02-06, by wenzelm
removed getplatform, ISABELLE_OUTPUT_DIR;
1997-02-06, by wenzelm
removed getplatform, ISABELLE_OUTPUT_DIR;
1997-02-06, by wenzelm
removed getplatform;
1997-02-06, by wenzelm
integrated getplatform stuff;
1997-02-06, by wenzelm
now falls back on ucat instead of cat;
1997-02-06, by wenzelm
improved usage msg;
1997-02-06, by wenzelm
added eq_sort (will move to sorts.ML eventually);
1997-02-06, by wenzelm
adapted to new Syntax.read_typ;
1997-02-06, by wenzelm
adapted read_typ, simple_read_typ;
1997-02-06, by wenzelm
improved comments;
1997-02-06, by wenzelm
added string_of_vname' (treats neg. index as free);
1997-02-06, by wenzelm
cd made readably again;
1997-02-06, by wenzelm
tuned;
1997-02-05, by wenzelm
Gradual switching to Basis Library functions nth, drop, etc.
1997-02-04, by paulson
now uses tee -i instead of perl;
1997-02-04, by wenzelm
now uses ISABELLE_INSTALLFONTS;
1997-02-04, by wenzelm
added ISABELLE_INSTALLFONTS;
1997-02-04, by wenzelm
Declaration of ccontr (classical contradiction) for HOL compatibility
1997-01-31, by paulson
Correction to Problem 24
1997-01-31, by paulson
Correction to Problem 24
1997-01-31, by paulson
Correction to Problem 24 (with unsatisfactory proof)
1997-01-31, by paulson
ex_impE was incorrectly listed as Safe
1997-01-31, by paulson
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
1997-01-31, by oheimb
added Classlib.* and Witness.*,
1997-01-31, by oheimb
moved Coind.*, Dagstuhl.*, Focus_ex.* to HOLCF/ex,
1997-01-31, by oheimb
added def_fix_ind and def_wfix_ind for convenience
1997-01-31, by oheimb
added addloop (and also documentation of addsolver
1997-01-31, by oheimb
changed handling of cont_lemmas and adm_lemmas
1997-01-31, by oheimb
fixed getplatform call;
1997-01-29, by wenzelm
removed warning for unprintable chars in strings (functionality will
1997-01-29, by wenzelm
The redeclaration of qed_spec_mp is unnecessary because it is now declared
1997-01-29, by paulson
Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
1997-01-29, by paulson
fixed problems with strange user .bashrc etc. (stty, ...);
1997-01-28, by wenzelm
Tidied unicity theorems
1997-01-27, by paulson
deepen_tac is NOT complete when made to apply "spec" as a safe rule\!\!
1997-01-27, by paulson
Corrected faulty comment
1997-01-27, by paulson
More news items, dating back to 1995
1997-01-27, by paulson
*** empty log message ***
1997-01-27, by wenzelm
*** empty log message ***
1997-01-24, by wenzelm
*** empty log message ***
1997-01-24, by wenzelm
Isabelle NEWS -- history of user-visible changes;
1997-01-24, by wenzelm
changed case symbol to \<Rightarrow>;
1997-01-24, by wenzelm
'rm -f' instead of 'mv -f';
1997-01-23, by wenzelm
Re-ordering of certificates so that session keys appear in decreasing order
1997-01-23, by paulson
Cosmetic improvements
1997-01-23, by paulson
'rm -f' instead of 'cp -f';
1997-01-23, by wenzelm
tuned;
1997-01-23, by wenzelm
expand shorthand goal commands;
1997-01-23, by wenzelm
added AxClasses test;
1997-01-23, by wenzelm
replaces README;
1997-01-23, by wenzelm
dummy file required for proper HTML generation;
1997-01-23, by wenzelm
removed;
1997-01-23, by wenzelm
removed \<mu> syntax;
1997-01-23, by wenzelm
added symbols syntax;
1997-01-23, by wenzelm
turned some consts into syntax;
1997-01-23, by wenzelm
Mended spelling error
1997-01-23, by paulson
Added sees_Spy_partsEs
1997-01-23, by paulson
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
1997-01-23, by paulson
Added warning msg when the simplifier cannot use a premise as a rewrite rule
1997-01-22, by nipkow
Modified MiniML. Added W0.
1997-01-21, by nipkow
Simplified proofs
1997-01-21, by paulson
Improved layout and updated comments
1997-01-21, by paulson
Improved text.
1997-01-20, by nipkow
Now requests runtimes of all theories
1997-01-20, by paulson
Simplified Oops case of main theorem
1997-01-20, by paulson
Documents the new command "prlim"
1997-01-20, by paulson
Added W0 and modified MiniML.
1997-01-17, by nipkow
Ball_Un -> ball_Un
1997-01-17, by nipkow
The new version of MiniML including "let".
1997-01-17, by nipkow
Algorithm I has not been ported to the polymorphic version yet.
1997-01-17, by nipkow
Updated documentation pointers.
1997-01-17, by nipkow
added gen_overwrite;
1997-01-17, by wenzelm
addsimps, addeqcongs: replaced @ by gen_union;
1997-01-17, by wenzelm
Incorporated Larry's changes.
1997-01-17, by nipkow
New rewrites for bounded quantifiers
1997-01-17, by paulson
This is the old version og MiniML for the monomorphic case.
1997-01-17, by nipkow
Modified some defs and shortened proofs.
1997-01-17, by nipkow
Now with Andy Gordon's treatment of freshness to replace newN/K
1997-01-17, by paulson
Deleted the redundant theorem subset_empty_iff (subset_empty exists already)
1997-01-17, by paulson
Added the prlim command
1997-01-17, by paulson
New miniscoping rules for the bounded quantifiers and UN/INT operators
1997-01-17, by paulson
Got rid of Alls in List.
1997-01-17, by nipkow
Got rid of Alls in favour of !x:set_of_list
1997-01-17, by nipkow
binary oprations and relations;
1997-01-16, by wenzelm
added termless parameter;
1997-01-16, by wenzelm
added term order;
1997-01-16, by wenzelm
improved error msg;
1997-01-13, by wenzelm
added datatype order;
1997-01-13, by wenzelm
added -? option;
1997-01-13, by wenzelm
replaced unit refs by 'stamp';
1997-01-13, by wenzelm
cleaned up (real changes next time);
1997-01-10, by wenzelm
make all Isabelle systems afresh;
1997-01-09, by wenzelm
*** empty log message ***
1997-01-09, by wenzelm
IsaMakefile for ZF;
1997-01-09, by wenzelm
Tidying of proofs. New theorems are enterred immediately into the
1997-01-09, by paulson
New theorem add_leE
1997-01-09, by paulson
New treatment of nonce creation
1997-01-09, by paulson
Removal of needless "addIs [equality]", etc.
1997-01-09, by paulson
New discussion of implicit simpsets & clasets
1997-01-08, by paulson
IsaMakefile for HOLCF;
1997-01-08, by wenzelm
Removal of sum_cs and eq_cs
1997-01-08, by paulson
IsaMakefile for Sequents;
1997-01-08, by wenzelm
IsaMakefile for CTT;
1997-01-08, by wenzelm
IsaMakefile for FOLP;
1997-01-08, by wenzelm
IsaMakefile for CCL;
1997-01-08, by wenzelm
IsaMakefile for LCF;
1997-01-08, by wenzelm
IsaMakefile for Cube;
1997-01-08, by wenzelm
Removed some (not all!) uses of FOL_cs
1997-01-08, by paulson
Simplification of some proofs, especially by eliminating
1997-01-07, by paulson
Incorporation of HPair into Message
1997-01-07, by paulson
Default rewrite rules for quantification over Collect(A,P)
1997-01-07, by paulson
Default rewrite rules for quantification over Collect(A,P)
1997-01-07, by paulson
Now uses HPair
1997-01-07, by paulson
Tidied up the unicity proofs
1997-01-07, by paulson
Updated account of implicit simpsets and clasets
1997-01-07, by paulson
added ISABELLE, ISATOOL;
1997-01-07, by wenzelm
testdir: use dir without committing into database;
1997-01-07, by wenzelm
added dvi viewer alternative;
1997-01-07, by wenzelm
fixed cmp -s option;
1997-01-07, by wenzelm
minor tuning;
1997-01-07, by wenzelm
minor tuning;
1997-01-07, by wenzelm
minor tuning;
1997-01-07, by wenzelm
added stamp util;
1997-01-06, by wenzelm
A definition of "print", unfortunately overridden by each "open PolyML"
1997-01-03, by paulson
Implicit simpsets and clasets for FOL and ZF
1997-01-03, by paulson
Added TFL
1997-01-03, by paulson
Conversion to Basis Library (using prs instead of output)
1997-01-03, by paulson
changed xterm geometry;
1996-12-20, by wenzelm
removed test
1996-12-20, by oheimb
testing...
1996-12-20, by oheimb
testing cvs merge algorithm, 2nd
1996-12-20, by sandnerr
testing...
1996-12-20, by oheimb
testing cvs merge algorithm
1996-12-20, by sandnerr
testing...
1996-12-20, by oheimb
testing: last line w/o nl
1996-12-20, by oheimb
testing: last line w/o nl
1996-12-20, by oheimb
testing...
1996-12-20, by oheimb
testing cvs update
1996-12-20, by oheimb
Simplification and generalization of the guarantees.
1996-12-20, by paulson
Corrected comments
1996-12-20, by paulson
corrected headers
1996-12-19, by oheimb
converted dist_less_one and dist_eq_one to single theorems instead of thm lists
1996-12-19, by oheimb
Extensive tidying and simplification, largely stemming from
1996-12-19, by paulson
Addition of Auth/Recur
1996-12-19, by paulson
Recursive Authentication Protocol
1996-12-18, by paulson
IsaMakefile for HOL;
1996-12-18, by wenzelm
removed unused symbol_input.pl
1996-12-18, by oheimb
The previous log message was wrong. The correct one is:
1996-12-18, by oheimb
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
1996-12-18, by oheimb
added cfst_strict and csnd_strict
1996-12-18, by oheimb
factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
1996-12-18, by oheimb
added qed_goal_spec_mp and qed_goalw_spec_mp
1996-12-18, by oheimb
added nat_induct2
1996-12-18, by oheimb
fixed EXIT def;
1996-12-18, by wenzelm
repaired some proofs
1996-12-18, by oheimb
little improvement for the handling of sort constraints:
1996-12-18, by oheimb
Isabelle make utility;
1996-12-18, by wenzelm
added ISABELLE_HTML;
1996-12-18, by wenzelm
added ISABELLE_HTML;
1996-12-18, by wenzelm
improved usage msg;
1996-12-18, by wenzelm
IsaMakefile for FOL;
1996-12-18, by wenzelm
minor modifications to accomodate IsaMakefile;
1996-12-18, by wenzelm
IsaMakefile for Pure Isabelle;
1996-12-18, by wenzelm
now refers to absolute paths of binaries;
1996-12-17, by wenzelm
fixed ML_HOME;
1996-12-17, by wenzelm
improved error handling;
1996-12-17, by wenzelm
Isabelle user settings sample;
1996-12-17, by wenzelm
major cleanup;
1996-12-17, by wenzelm
Poly/ML style prompts;
1996-12-17, by wenzelm
fixed Title;
1996-12-16, by wenzelm
added consistency comment
1996-12-16, by oheimb
added consistency comment
1996-12-16, by oheimb
repaired several proofs
1996-12-16, by oheimb
corrected 8bit symbols
1996-12-16, by oheimb
tuned read and write functions;
1996-12-16, by wenzelm
New tactics: prove_unique_tac and analz_induct_tac
1996-12-16, by paulson
New tactic: prove_unique_tac
1996-12-16, by paulson
Removed a rogue TAB
1996-12-16, by paulson
New tactic: prove_unique_tac
1996-12-16, by paulson
intro_tacsf: replaced ORELSE by APPEND in order to stop
1996-12-16, by paulson
SML/NJ startup script (for 0.93).
1996-12-16, by wenzelm
fixed \<subseteq> input;
1996-12-16, by wenzelm
SML/NJ startup script (for 0.93).
1996-12-16, by wenzelm
added smlnj-0.93;
1996-12-16, by wenzelm
Compatibility file for Standard ML of New Jersey, version 1.07.
1996-12-16, by wenzelm
added needs_filtered_use;
1996-12-16, by wenzelm
added write_charnames';
1996-12-16, by wenzelm
now uses SymbolInput.use;
1996-12-16, by wenzelm
symbol_input.ML: Defines 'use' command with symbol input filtering.
1996-12-16, by wenzelm
added symbol_input.ML;
1996-12-16, by wenzelm
fixed comment;
1996-12-16, by wenzelm
fixed comments;
1996-12-16, by wenzelm
now passes ML_SYSTEM as ml_system;
1996-12-16, by wenzelm
added symbolinput filter;
1996-12-16, by wenzelm
symbolinput - translate symbols into \<...> sequences;
1996-12-16, by wenzelm
renamed to symbolinput.pl;
1996-12-16, by wenzelm
renamed from symbol_input.pl;
1996-12-16, by wenzelm
minor tuning;
1996-12-16, by wenzelm
now fails if getsettings not found;
1996-12-16, by wenzelm
adaptions for symbol font
1996-12-13, by oheimb
adaptions for symbol font
1996-12-13, by oheimb
minor adaptions
1996-12-13, by oheimb
added header
1996-12-13, by oheimb
now also loads etc/isa-settings.el;
1996-12-13, by wenzelm
now discgarb called only for changed databases;
1996-12-13, by wenzelm
added set inclusion symbol syntax;
1996-12-13, by wenzelm
added warning for unprintable chars in strings;
1996-12-13, by wenzelm
fixed warning;
1996-12-13, by wenzelm
added typed print translations;
1996-12-13, by wenzelm
removed chartrans_of;
1996-12-13, by wenzelm
added extend_trfunsT;
1996-12-13, by wenzelm
added fix_tr', syn_ext_trfunsT;
1996-12-13, by wenzelm
binder_tr': applied fix_tr';
1996-12-13, by wenzelm
Dummy change to document the change in revision 1.5:
1996-12-13, by sandnerr
ex/Hoare.thy
1996-12-13, by sandnerr
Removed needless quotation marks
1996-12-13, by paulson
Streamlined many proofs
1996-12-13, by paulson
Temporary additions (random) for the nested Otway-Rees protocol
1996-12-13, by paulson
Streamlined some proofs
1996-12-13, by paulson
Streamlined many proofs
1996-12-13, by paulson
Addition of the Hash constructor
1996-12-13, by paulson
fixed alternative quantifier symbol syntax;
1996-12-10, by wenzelm
Now target "test" builds and tests TFL
1996-12-10, by paulson
ROOT file for TFL (needed for use_dir to work)
1996-12-10, by paulson
removed ambiguous symbols syntax;
1996-12-10, by wenzelm
fixed pris of binder syntax;
1996-12-10, by wenzelm
fixed pris of binder syntax;
1996-12-10, by wenzelm
added chartrans;
1996-12-10, by wenzelm
added chartrans_of;
1996-12-10, by wenzelm
mfix_to_xprod: now uses read_charnames;
1996-12-10, by wenzelm
tokenize: no gets exploded char list;
1996-12-10, by wenzelm
added read_charnames, write_charnames;
1996-12-10, by wenzelm
*** empty log message ***
1996-12-10, by wenzelm
syntax section: added 'output' mode option;
1996-12-10, by wenzelm
add_modesyntax(_i): added 'inout' argument;
1996-12-10, by wenzelm
symbol_input.pl - translate symbols into \<...> sequences.
1996-12-10, by wenzelm
Headers added
1996-12-09, by sandnerr
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
1996-12-09, by sandnerr
simpset extension moved from HOLCF.ML to One.ML and Tr2.ML
1996-12-09, by sandnerr
added theorems
1996-12-09, by sandnerr
qed_spec_mp moved to end of file
1996-12-09, by sandnerr
added DVI_VIEWER for 600dpi fonts;
1996-12-09, by wenzelm
Contents - list of available documentation;
1996-12-09, by wenzelm
patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
1996-12-09, by wenzelm
various fixes;
1996-12-09, by wenzelm
*** empty log message ***
1996-12-09, by wenzelm
added -norc option;
1996-12-09, by wenzelm
getplatform - bash source script to augment current env;
1996-12-09, by wenzelm
added ISABELLE_DOCS;
1996-12-09, by wenzelm
added -norc option;
1996-12-09, by wenzelm
added -norc option;
1996-12-09, by wenzelm
Compatibility file for Standard ML of New Jersey, version 1.09.
1996-12-09, by wenzelm
Compatibility file for Poly/ML (versions 2.x, 3.x).
1996-12-09, by wenzelm
*** empty log message ***
1996-12-09, by wenzelm
mk - build Pure Isabelle.
1996-12-09, by wenzelm
removed escaping of 8bit chars;
1996-12-09, by wenzelm
comitting symlinks failed!!!
1996-12-09, by wenzelm
renamed from POLY.ML;
1996-12-09, by wenzelm
added -norc option;
1996-12-09, by wenzelm
added -norc option;
1996-12-09, by wenzelm
findlogics: collect heap names from ISABELLE_PATH;
1996-12-09, by wenzelm
doc: view Isabelle documentation;
1996-12-09, by wenzelm
Minor renamings
1996-12-06, by paulson
MLWorks compatibility: it sort of works
1996-12-06, by paulson
Added public-key examples for Auth
1996-12-06, by paulson
Minor renamings
1996-12-06, by paulson
Moved much common material to Message.ML
1996-12-05, by paulson
Updating of banner
1996-12-05, by paulson
Loads new public-key examples
1996-12-05, by paulson
Minor speedups
1996-12-05, by paulson
Trivial renamings
1996-12-05, by paulson
Trivial renamings
1996-12-05, by paulson
Updated a comment
1996-12-05, by paulson
Moved much common material to Message.ML
1996-12-05, by paulson
Updating of comments
1996-12-05, by paulson
Public-key examples
1996-12-05, by paulson
added pwd;
1996-12-05, by wenzelm
fixed commit emulation;
1996-12-04, by wenzelm
changed font menu;
1996-12-04, by wenzelm
replaced cat by ucat;
1996-12-04, by wenzelm
replaced cat by ucat;
1996-12-04, by wenzelm
*** empty log message ***
1996-12-04, by wenzelm
fails more gracefully;
1996-12-04, by wenzelm
fixed ML_HOME;
1996-12-04, by wenzelm
added ISAMODE_HOME;
1996-12-04, by wenzelm
improved 'not found' messages;
1996-12-04, by wenzelm
*** empty log message ***
1996-12-04, by wenzelm
ucat - uninterruptible cat
1996-12-04, by wenzelm
Emacs / Isamode interface.
1996-12-03, by wenzelm
Simplified file_info using OS.FileSys instead of Posix.FileSys
1996-12-03, by paulson
Random number generated "downgraded" to generate numbers below 2^29 - 1,
1996-12-03, by paulson
run-smlnj: SML/NJ startup script (for 1.06 or later).
1996-12-02, by wenzelm
run-polyml: Poly/ML startup script.
1996-12-02, by wenzelm
isa-xterm: Isabelle within an xterm.
1996-12-02, by wenzelm
getsettings: bash source script to augment current env.
1996-12-02, by wenzelm
isabelle symbol fonts;
1996-12-02, by wenzelm
installfonts: install Isabelle symbol fonts.
1996-12-02, by wenzelm
getenv: get value from Isabelle settings.
1996-12-02, by wenzelm
changeparent: change parent of Poly/ML database.
1996-12-02, by wenzelm
settings: Isabelle settings -- site defaults.
1996-12-02, by wenzelm
isatool: Isabelle tool starter -- keeps your PATH name space clean.
1996-12-02, by wenzelm
isabelle: Basic Isabelle startup script.
1996-12-02, by wenzelm
removed 8bit sections
1996-12-02, by oheimb
replaced Lift3 by Up3, moving Lift3.p to Up3.p
1996-12-02, by oheimb
in Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg
1996-12-02, by oheimb
Made comments more explicit
1996-12-02, by paulson
Removal of needless occurrences of "op"
1996-12-02, by paulson
removed out-dated comment;
1996-12-02, by wenzelm
removed;
1996-12-02, by wenzelm
Swapped arguments of Crypt (for clarity and because it is conventional)
1996-11-29, by paulson
Swapping arguments of Crypt; removing argument lost
1996-11-29, by paulson
added qed_spec_mp (from HOL);
1996-11-29, by wenzelm
Ring Theory.
1996-11-29, by nipkow
Moved the Rings stuff from ex to Integ and showed that int::cring.
1996-11-29, by nipkow
Modified dependencies for ex and Integ. (Rings)
1996-11-29, by nipkow
*** empty log message ***
1996-11-29, by oheimb
moved Lift*.* to Up*.*, renaming of all constans and theorems concerned,
1996-11-29, by oheimb
modified file headers
1996-11-29, by oheimb
renamed is_flat to flat,
1996-11-29, by oheimb
Addition of Woo-Lam protocol
1996-11-28, by paulson
Fixed spelling error
1996-11-28, by paulson
Tidying and renaming of function Dom
1996-11-28, by paulson
Declares List_ as a synonym for List
1996-11-28, by paulson
Replaced map...~~ by ListPair.map
1996-11-28, by paulson
Extra fix needed in newN case
1996-11-28, by paulson
Missing case in instantiation of Transitivity prover (negate(None)=None)
1996-11-28, by nipkow
Replaced map...~~ by ListPair.map
1996-11-28, by paulson
Replaced map...~~ by ListPair.map
1996-11-28, by paulson
Addition of structures List and ListPair
1996-11-28, by paulson
Weaking of injectivity assumptions for newK and newN:
1996-11-28, by paulson
moved split_tac
1996-11-27, by oheimb
added symbols syntax;
1996-11-27, by wenzelm
added "op :", "op ~:" syntax;
1996-11-27, by wenzelm
added symbols syntax;
1996-11-27, by wenzelm
fixed comment;
1996-11-27, by wenzelm
moved "1", "2" to syntax section;
1996-11-27, by wenzelm
symbol names changes;
1996-11-27, by wenzelm
symbol name changes;
1996-11-27, by wenzelm
improved some symbol names;
1996-11-27, by wenzelm
changed symbolic char syntax to \<NAME>
1996-11-27, by wenzelm
use_thy now automatically opens theory structures;
1996-11-27, by wenzelm
renamed "symbolfont" to "symbols";
1996-11-27, by wenzelm
moved if_cancel to the right place
1996-11-27, by oheimb
added if_cancel later to simpset
1996-11-27, by oheimb
Updated instructions
1996-11-27, by paulson
Better indentation
1996-11-27, by paulson
Replaced obsolete "use" command
1996-11-27, by paulson
Compatibility with SML/NJ 109, and some compatibility with later versions
1996-11-27, by paulson
Now tries to delete SML/NJ .heap files
1996-11-27, by paulson
Converted I/O operatios for Basis Library compatibility
1996-11-27, by paulson
Eta-expanded some declarations that are illegal under value polymorphism
1996-11-27, by paulson
Basis library emulation, especially of I/O operations
1996-11-27, by paulson
Removed an obsolete and incompatible declaration
1996-11-27, by paulson
Replaced obsolete "makestring" by Bool.toString
1996-11-27, by paulson
Replaced obsolete "makestring" by Int.toString
1996-11-27, by paulson
Eta-expanded some declarations that are illegal under value polymorphism
1996-11-27, by paulson
Replaced obsolete "use" command
1996-11-27, by paulson
less
more
|
(0)
-1000
-384
+384
+1000
+3000
+10000
+30000
tip