isabelle: Graph

added -b option (batch mode);
1997-04-04, by wenzelm
renamed variable 'inv'
1997-04-04, by nipkow
added Quot examples;
1997-04-04, by wenzelm
*** empty log message ***
1997-04-04, by wenzelm
Higher-order quotients.
1997-04-04, by wenzelm
Now calls blast_tac
1997-04-04, by paulson
Another blast_tac call
1997-04-04, by paulson
Simplified a proof
1997-04-04, by paulson
Re-organization of the order of haz rules
1997-04-04, by paulson
Calls Blast_tac. Tidied some proofs
1997-04-04, by paulson
Calls Blast_tac. Tidied some proofs
1997-04-04, by paulson
Calls Blast_tac
1997-04-04, by paulson
Adds image_eqI instead of imageI, as the former is more general
1997-04-04, by paulson
Added blast.ML as a dependency
1997-04-04, by paulson
Now calls Blast_tac and has some hard examples (Halting Problem
1997-04-04, by paulson
Only layout mods.
1997-04-03, by nipkow
Now: unit = {True}
1997-04-03, by nipkow
Two extra commands shorten the proof time by 800 seconds...
1997-04-03, by paulson
More List and ListPair utilities
1997-04-03, by paulson
Now exports declConsts!
1997-04-03, by paulson
Declares overloading for if-and-only-if
1997-04-03, by paulson
Declares overloading for set-theoretic constants
1997-04-03, by paulson
Removed (Unit) in Prod.
1997-04-03, by nipkow
misc improvements;
1997-04-02, by wenzelm
changed signature of dummy goal from proto_pure to pure;
1997-04-02, by wenzelm
Converted to call blast_tac.
1997-04-02, by paulson
Uses ZF.thy again, to make that theory usable
1997-04-02, by paulson
Mostly converted to blast_tac
1997-04-02, by paulson
Datatype declarations now require theory Datatype--NOT in quotes
1997-04-02, by paulson
Converted back from upair.thy to ZF.thy
1997-04-02, by paulson
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
1997-04-02, by paulson
Now checks for existence of theory Inductive (Fixedpt was too small)
1997-04-02, by paulson
Now a non-trivial theory so that require_thy can find it
1997-04-02, by paulson
DEEPEN now takes an upper bound for terminating searches
1997-04-02, by paulson
New DEEPEN allows giving an upper bound for deepen_tac
1997-04-02, by paulson
Now builds blast_tac
1997-04-02, by paulson
Now loads blast.ML
1997-04-02, by paulson
ZF.thy is again usable
1997-04-02, by paulson
The isabelle-0 encoding table.
1997-04-02, by wenzelm
Made the error message more explicit
1997-04-02, by paulson
Now declares Basis Library version of type option
1997-04-02, by paulson
Replaced Best_tac by the one rule needed for the proof
1997-04-02, by paulson
Installation of blast_tac
1997-04-02, by paulson
Now tests for essential ancestors (Lfp or Gfp)
1997-04-02, by paulson
Re-ordering of rules to assist blast_tac
1997-04-02, by paulson
Now loads blast_tac
1997-04-02, by paulson
Reorganization of how classical rules are installed
1997-04-02, by paulson
Now calls require_thy to ensure ancestors are present
1997-04-02, by paulson
Implementation of blast_tac: fast tableau prover
1997-04-02, by paulson
replaced by usedir;
1997-04-01, by wenzelm
eliminated references to old 8bit fonts;
1997-04-01, by wenzelm
improved messages;
1997-04-01, by wenzelm
removed useless symbol font syntax;
1997-04-01, by wenzelm
fixed -s option;
1997-04-01, by wenzelm
simple_ast_of: fixed handling of loose Bounds;
1997-03-31, by wenzelm
Replaced (s,t) : id by s=t.
1997-03-30, by nipkow
Optimized proofs.
1997-03-27, by nipkow
Changes made necessary by the new ex1 rules
1997-03-27, by paulson
Now uses the alternative (safe!) rules for ex1
1997-03-27, by paulson
Updated comment
1997-03-27, by paulson
Cleaned up a little.
1997-03-26, by nipkow
Added "discrete" CPOs and modified IMP to use those rather than "lift"
1997-03-26, by nipkow
generalized theorems and class instances for Cprod.
1997-03-26, by slotosch
changed some theorems from pcpo to cpo
1997-03-25, by slotosch
changed continuous functions from pcpo to cpo (including instances)
1997-03-25, by slotosch
Trivial renamings (for consistency with CSFW papers)
1997-03-25, by paulson
Toby's better treatment of eta-contraction
1997-03-25, by paulson
Deleted needless parentheses
1997-03-24, by paulson
Deleted unnecessary rules
1997-03-24, by paulson
fixed font names;
1997-03-20, by wenzelm
exit_use_dir;
1997-03-20, by wenzelm
isatool usedir;
1997-03-20, by wenzelm
exit_use_dir;
1997-03-20, by wenzelm
remove empty dirs;
1997-03-20, by wenzelm
isatool usedir;
1997-03-20, by wenzelm
improved session names;
1997-03-20, by wenzelm
isatool usedir;
1997-03-20, by wenzelm
*** empty log message ***
1997-03-20, by wenzelm
tuned;
1997-03-20, by wenzelm
isatool usedir;
1997-03-20, by wenzelm
exit_use_dir;
1997-03-20, by wenzelm
isatool usedir;
1997-03-20, by wenzelm
replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
1997-03-20, by wenzelm
isatool usedir;
1997-03-20, by wenzelm
added ex dir;
1997-03-20, by wenzelm
replaced ex.ML by ex/ROOT.ML, ex/ex.ML;
1997-03-20, by wenzelm
replaced ex.ML by ex/ROOT.ml, ex/ex.ML;
1997-03-20, by wenzelm
Improved intersection rule InterI: now truly safe, since the unsafeness is
1997-03-19, by paulson
delete_tagged_brl just ignores non-elimination rules instead of complaining
1997-03-19, by paulson
delrules now deletes ALL occurrences of a rule, since it may appear in any of
1997-03-19, by paulson
added quit();
1997-03-18, by wenzelm
asserts $ISABELLE_OUTPUT_DIR;
1997-03-18, by wenzelm
Added wp_while.
1997-03-18, by nipkow
added dummy set_session;
1997-03-18, by wenzelm
usedir -- build object-logic or run examples;
1997-03-18, by wenzelm
A more explicit prefix because gensym now generates easily predicatable
1997-03-18, by paulson
gensym no longer generates random identifiers, but just enumerates them
1997-03-18, by paulson
Made the indentation rational
1997-03-18, by paulson
fixed Tools path;
1997-03-18, by wenzelm
Conducted the IFOL proofs using intuitionistic tools
1997-03-18, by paulson
Stopped giving Introduction rules as Elimination rules
1997-03-18, by paulson
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
1997-03-18, by nipkow
Added P&P&Q = P&Q and P|P|Q = P|Q.
1997-03-18, by nipkow
*** empty log message ***
1997-03-17, by nipkow
The HOLCF-based den. sem. of IMP.
1997-03-17, by nipkow
Added the HOLCF-based den. sem. of IMP.
1997-03-17, by nipkow
Added link to HOLCF/IMP
1997-03-17, by nipkow
fixed perl path;
1997-03-17, by wenzelm
uncommented chown / chmod (again);
1997-03-17, by wenzelm
Modified proofs because simplifier does not eta-contract any longer.
1997-03-14, by nipkow
Avoid eta-contraction in the simplifier.
1997-03-14, by nipkow
tuned glyphs;
1997-03-11, by wenzelm
tuned Sigma glyph;
1997-03-11, by wenzelm
major tuning;
1997-03-11, by wenzelm
tuned comments;
1997-03-11, by wenzelm
tuned comments;
1997-03-11, by wenzelm
tuned comments;
1997-03-11, by wenzelm
tuned;
1997-03-11, by wenzelm
tuned comment;
1997-03-11, by wenzelm
Note on fonts and remote X11;
1997-03-11, by wenzelm
tr is (again) type abbrev;
1997-03-11, by wenzelm
added THIS_IS_ISABELLE_BUILD;
1997-03-11, by wenzelm
added THIS_IS_ISABELLE_BUILD discrimination;
1997-03-11, by wenzelm
The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac
1997-03-10, by paulson
renamed;
1997-03-07, by wenzelm
fixed;
1997-03-07, by wenzelm
commented out chwon, chmod;
1997-03-07, by wenzelm
fixed src path;
1997-03-07, by wenzelm
added \n at EOF;
1997-03-07, by wenzelm
*** empty log message ***
1997-03-07, by wenzelm
tuned;
1997-03-07, by wenzelm
renamed fonts;
1997-03-07, by wenzelm
renamed font;
1997-03-07, by wenzelm
removed lparr, rparr, empty, succeq, ge, rrightarrow;
1997-03-07, by wenzelm
renamed SYSTEM to RAW_ML_SYSTEM;
1997-03-07, by wenzelm
added \<Colon> syntax for constraints (more compact!);
1997-03-07, by wenzelm
"bool lift" now syntax instead of type abbrev;
1997-03-07, by wenzelm
*** empty log message ***
1997-03-07, by wenzelm
added atac 2 (again);
1997-03-07, by wenzelm
removed (| |) symbols syntax;
1997-03-07, by wenzelm
fixed Not syntax;
1997-03-07, by wenzelm
tuned comment;
1997-03-07, by wenzelm
tuned comments;
1997-03-07, by wenzelm
Isabelle installation notes;
1997-03-07, by wenzelm
now sans serifs;
1997-03-07, by wenzelm
tuned;
1997-03-07, by wenzelm
*** empty log message ***
1997-03-07, by wenzelm
build - compile parts of the Isabelle system;
1997-03-07, by wenzelm
moved settings comment to build;
1997-03-07, by wenzelm
Removed some polymorphic equality tests
1997-03-07, by paulson
Improved indentation of aconv
1997-03-07, by paulson
Corrected aeconv and exported it
1997-03-07, by paulson
Prevent permutation of assumptions in hyp_subst_tac
1997-03-07, by paulson
Deleted steps made redundant by the stronger eq_assume_tac
1997-03-07, by paulson
Eta-expanded some declarations for compatibility with value polymorphism
1997-03-07, by paulson
Tidied and updated
1997-03-07, by paulson
more robust check;
1997-03-07, by wenzelm
renamed, improved, augmented version of isabelle fonts;
1997-03-07, by wenzelm
tuned comment;
1997-03-07, by wenzelm
tuned;
1997-03-07, by wenzelm
pass xterm mode by default;
1997-03-07, by wenzelm
Minor changes due to primrec definition for ^
1997-03-06, by pusch
primrec definition for ^
1997-03-06, by pusch
Minor changes due to primrec definition for nth
1997-03-06, by pusch
primrec definition for nth
1997-03-06, by pusch
Oops, forgot to remove -x again;
1997-03-06, by wenzelm
added ISABELLE_HOME normalization;
1997-03-06, by wenzelm
even more robust and user friendly invocation (no longer requieres
1997-03-06, by wenzelm
improved DESCRIPTION;
1997-03-05, by wenzelm
added -a, -b options;
1997-03-05, by wenzelm
*** empty log message ***
1997-03-05, by wenzelm
*** empty log message ***
1997-03-05, by wenzelm
*** empty log message ***
1997-03-05, by wenzelm
Added comment
1997-03-05, by paulson
Now uses eta_contract_atom for greater speed
1997-03-05, by paulson
Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
1997-03-05, by paulson
HOL: renaming of "not"
1997-03-05, by paulson
Declares eta_contract_atom; fixed comment; some tidying
1997-03-05, by paulson
Added comment
1997-03-05, by paulson
Now declares needs_filtered_use, but still unusable with current MLWorks
1997-03-05, by paulson
Now uses rotate_tac and eta_contract_atom for greater speed
1997-03-05, by paulson
New version of InterE, like its ZF counterpart
1997-03-05, by paulson
Renamed constant "not" to "Not"
1997-03-05, by paulson
Renamed constant "not" to "Not"
1997-03-04, by paulson
Renamed constant "not" to "Not"
1997-03-04, by paulson
best_tac avoids looping with change to RepFun_eqI in claset
1997-03-04, by paulson
Now uses RepFun_eqI instead of RepFunI;
1997-03-04, by paulson
Updated reference to Pelletier erratum
1997-03-04, by paulson
Removed needless quotes
1997-03-04, by paulson
removed bash debug;
1997-03-03, by wenzelm
removed -r option;
1997-03-03, by wenzelm
fixed -m order;
1997-03-03, by wenzelm
improved xterm, xterm_color;
1997-03-03, by wenzelm
added comment;
1997-03-03, by wenzelm
added comment: print translations do not mark tokens;
1997-03-03, by wenzelm
added color styles;
1997-03-01, by wenzelm
improved err msg;
1997-02-28, by wenzelm
*** empty log message ***
1997-02-28, by wenzelm
more robust handling of invocation errors;
1997-02-28, by wenzelm
more robust handling of invocation errors;
1997-02-28, by wenzelm
now uses -m symbols;
1997-02-28, by wenzelm
split ast_of_term(T);
1997-02-28, by wenzelm
added token translation support;
1997-02-28, by wenzelm
term_of_... now mark class, tfree, tvar;
1997-02-28, by wenzelm
added mark_bound(T), variant_abs';
1997-02-28, by wenzelm
Token translations for xterm and LaTeX output.
1997-02-28, by wenzelm
added _mk_ofclass(S);
1997-02-28, by wenzelm
added strlen (includes metric information);
1997-02-28, by wenzelm
added token_translation interface;
1997-02-28, by wenzelm
added add_tokentrfuns;
1997-02-28, by wenzelm
added Syntax/token_trans.ML;
1997-02-28, by wenzelm
added token_trans.ML;
1997-02-28, by wenzelm
Slightly more robust proof
1997-02-28, by paulson
dup_intr & dup_elim no longer call standard -- this
1997-02-28, by paulson
rule_by_tactic no longer standardizes its result
1997-02-28, by paulson
Addition of de Bruijn formulae
1997-02-28, by paulson
tuned comment;
1997-02-27, by wenzelm
tuned comments;
1997-02-27, by wenzelm
added proper subset symbols syntax;
1997-02-25, by wenzelm
minor changes due to primrec defintions for +,-,*
1997-02-25, by pusch
minor changes due to new primrec definitions for +,-,*
1997-02-25, by pusch
definitions of +,-,* replaced by primrec definitions
1997-02-25, by pusch
function nat_add_primrec added to allow primrec definitions over nat
1997-02-25, by pusch
removed explicit_domains/, which is now covered by ex/
1997-02-24, by oheimb
added "_" syntax for dummyT;
1997-02-24, by wenzelm
declared the dummy type;
1997-02-21, by wenzelm
replaced natural by subset;
1997-02-21, by wenzelm
tuned symbolic [|_|] syntax;
1997-02-21, by wenzelm
tuned some chars;
1997-02-21, by wenzelm
More robust proof (?)
1997-02-21, by paulson
Replaced "flat" by the Basis Library function List.concat
1997-02-21, by paulson
Introduction of rotate_rule
1997-02-21, by paulson
removed empty line (which broke xfedor);
1997-02-21, by wenzelm
don't hack, use xfed or xfedor;
1997-02-21, by wenzelm
fixed Id comment;
1997-02-21, by wenzelm
makedist -- make Isabelle distribution.
1997-02-20, by wenzelm
tuned URL;
1997-02-20, by wenzelm
added index info;
1997-02-20, by wenzelm
index info;
1997-02-20, by wenzelm
added dist;
1997-02-20, by wenzelm
some administrative tools for the Isabelle;
1997-02-20, by wenzelm
made a bit more robust for 'make dist';
1997-02-20, by wenzelm
rail output;
1997-02-20, by wenzelm
fixed rail.sty dep;
1997-02-20, by wenzelm
added this file;
1997-02-20, by wenzelm
rail output;
1997-02-20, by wenzelm
made a bit more robust;
1997-02-20, by wenzelm
manual steps comment;
1997-02-17, by wenzelm
*** empty log message ***
1997-02-17, by wenzelm
described changes for HOLCF-Version without rules and arities
1997-02-17, by slotosch
file moved;
1997-02-17, by wenzelm
file moved here;
1997-02-17, by wenzelm
configure - adapt Isabelle distribution to system environment
1997-02-17, by wenzelm
improved description of recent changes
1997-02-17, by oheimb
reflecting recent changes of the simplifier
1997-02-17, by slotosch
corrected type of plift
1997-02-17, by oheimb