Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-1000
-480
+480
+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.
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
reflecting recent changes of the simplifier
1997-02-17, by oheimb
mk_rews: automatically includes strip_shyps, zero_var_indexes;
1997-02-17, by wenzelm
New file for theorems of Porder0
1997-02-17, by slotosch
tuned comments;
1997-02-17, by wenzelm
Examples are adopted to the changes from HOLCF.
1997-02-17, by slotosch
using types one = unit lift and translations causes troubles between
1997-02-17, by slotosch
Changes of HOLCF from Oscar Slotosch:
1997-02-17, by slotosch
*** empty log message ***
1997-02-15, by oheimb
reflecting my recent changes of the classical reasoner
1997-02-15, by oheimb
reflecting my recent changes of the simplifier and classical reasoner
1997-02-15, by oheimb
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
1997-02-15, by oheimb
cosmetic
1997-02-15, by oheimb
updated mini_ss
1997-02-15, by oheimb
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
1997-02-15, by oheimb
corrected minor mistakes
1997-02-15, by oheimb
description of safe vs. unsafe wrapper and the functions involved
1997-02-15, by oheimb
moved THEN_MAYBE to Pure/tctical.ML
1997-02-15, by oheimb
added deleqcongs, richer rep_ss
1997-02-15, by oheimb
description of del(eq)congs, safe and unsafe solver
1997-02-15, by oheimb
added THEN_MAYBE and THEN_MAYBE'
1997-02-15, by oheimb
added del_congs
1997-02-15, by oheimb
Some lemmas changed to valuesd
1997-02-14, by narasche
fixed comment;
1997-02-14, by wenzelm
improved interface options;
1997-02-14, by wenzelm
semi fix of piping-quit peoblem (should work on systems with *real* sh);
1997-02-14, by wenzelm
globally unset ENV, BASH_ENV;
1997-02-14, by wenzelm
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
less
more
|
(0)
-1000
-480
+480
+1000
+3000
+10000
+30000
tip