Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-1920
+1920
+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.
more monotonicity laws for times
1999-07-09, by paulson
products of signs as equivalences
1999-07-09, by paulson
-B option;
1999-07-08, by wenzelm
removed old version;
1999-07-08, by wenzelm
tuned indentation;
1999-07-08, by wenzelm
added export_chain;
1999-07-08, by wenzelm
propp: 'concl' patterns;
1999-07-08, by wenzelm
propp: 'concl' patterns;
1999-07-08, by wenzelm
terminal_proof: 2nd method;
1999-07-08, by wenzelm
'export';
1999-07-08, by wenzelm
propp: 'concl' patterns;
1999-07-08, by wenzelm
propp: 'concl' patterns;
1999-07-08, by wenzelm
improved error msgs of cterm_instantiate;
1999-07-08, by wenzelm
aprop: ??id, ...;
1999-07-08, by wenzelm
improved error msgs of instantiate;
1999-07-08, by wenzelm
added commute: 'a seq list -> 'a list seq;
1999-07-08, by wenzelm
added pretty_thm_no_hyps;
1999-07-08, by wenzelm
theorems involving oracles are now printed with a suffixed [!];
1999-07-08, by wenzelm
Theorems involving oracles will be printed with a suffixed \verb|[!]|;
1999-07-08, by wenzelm
updated usedir;
1999-07-08, by wenzelm
integer division
1999-07-08, by paulson
Renaming of theorems from _nat0 to _int0 and _nat1 to _int1
1999-07-08, by paulson
Introduction of integer division algorithm
1999-07-08, by paulson
changed header to cope with default if_weak_cong
1999-07-08, by paulson
Now if_weak_cong is a standard congruence rule
1999-07-08, by paulson
Introduction of integer division algorithm
1999-07-08, by paulson
tidied proofs to cope with default if_weak_cong
1999-07-08, by paulson
Now if_weak_cong is a standard congruence rule
1999-07-08, by paulson
new theory IntDiv.thy
1999-07-08, by paulson
new files IntDiv.{thy,ML}
1999-07-08, by paulson
tuned output;
1999-07-07, by wenzelm
simp only: attribute, method arg;
1999-07-06, by wenzelm
use generic numeral encoding and syntax;
1999-07-06, by wenzelm
adapted to generic numerals;
1999-07-06, by wenzelm
simp only;
1999-07-06, by wenzelm
added Numeral.thy;
1999-07-06, by wenzelm
_reflcl;
1999-07-06, by wenzelm
added Numeral.thy, Tools/numeral_syntax.ML;
1999-07-06, by wenzelm
removed proof history nesting commands (not useful);
1999-07-06, by wenzelm
improved errors;
1999-07-06, by wenzelm
removed nesting (unused);
1999-07-06, by wenzelm
export term_of_typ;
1999-07-06, by wenzelm
begin_theory: disallow finished;
1999-07-06, by wenzelm
added clear_mss;
1999-07-06, by wenzelm
variant version;
1999-07-05, by wenzelm
fixed scope of x:??H;
1999-07-04, by wenzelm
close_block: transfer_used_names;
1999-07-04, by wenzelm
added transfer_used_names;
1999-07-04, by wenzelm
oops;
1999-07-03, by wenzelm
proper text;
1999-07-03, by wenzelm
tuned;
1999-07-03, by wenzelm
tuned print_state;
1999-07-03, by wenzelm
fixed 'txt';
1999-07-03, by wenzelm
pretty_thm: include oracles (!) in hyps;
1999-07-03, by wenzelm
skip_proof feature 'sorry' (for quick_and_dirty mode only);
1999-07-02, by wenzelm
generalized fixes get index 0;
1999-07-02, by wenzelm
added 'txt';
1999-07-02, by wenzelm
add_txt;
1999-07-02, by wenzelm
tuned;
1999-07-02, by wenzelm
fixed order_trans;
1999-07-01, by wenzelm
added KnasterTarski.thy;
1999-07-01, by wenzelm
renamed with/APP to of/OF;
1999-07-01, by wenzelm
Isar_examples/KnasterTarski.thy;
1999-07-01, by wenzelm
added with_facts(_i);
1999-07-01, by wenzelm
'with' as == 'from' as facts;
1999-07-01, by wenzelm
also, finally: opt_rules;
1999-07-01, by wenzelm
have_thmss: more_ths;
1999-07-01, by wenzelm
have_thmss: more_ths;
1999-07-01, by wenzelm
renamed with/APP to of/OF;
1999-07-01, by wenzelm
tuned;
1999-07-01, by wenzelm
fixed backtracking of global_qed;
1999-07-01, by wenzelm
added check_result;
1999-07-01, by wenzelm
setmp Display.show_hyps false;
1999-07-01, by wenzelm
fix, assume, presume: prf_asm;
1999-07-01, by wenzelm
added prf_asm;
1999-07-01, by wenzelm
expandshort
1999-07-01, by paulson
many new theorems concerning multiplication and (in)equations
1999-07-01, by paulson
now div and mod are overloaded; dvd is polymorphic
1999-07-01, by paulson
new laws mult_le_cancel1, mult_le_cancel2
1999-07-01, by paulson
antisym first;
1999-06-30, by wenzelm
more robust trans rules;
1999-06-30, by wenzelm
Isar.sync_main;
1999-06-30, by wenzelm
added sync;
1999-06-30, by wenzelm
sync token;
1999-06-30, by wenzelm
sync;
1999-06-30, by wenzelm
added sync marker;
1999-06-30, by wenzelm
New thm trancl_trans_induct
1999-06-30, by nipkow
Bad translation fixed.
1999-06-29, by nipkow
updated;
1999-06-28, by wenzelm
improved RANGE;
1999-06-28, by wenzelm
tuned;
1999-06-28, by wenzelm
cond_extern_table;
1999-06-28, by wenzelm
added presume command;
1999-06-28, by wenzelm
cond_extern_table;
1999-06-28, by wenzelm
tuned print_state;
1999-06-28, by wenzelm
tuned output: print_context replaced by strings_of_context;
1999-06-28, by wenzelm
cond_extern_table;
1999-06-28, by wenzelm
added cond_extern_table;
1999-06-28, by wenzelm
branching_level = 400;
1999-06-25, by wenzelm
tidied
1999-06-23, by paulson
renamed PPI to plam
1999-06-23, by paulson
renamed PPI to plam
1999-06-23, by paulson
another non-working snapshot
1999-06-23, by paulson
new distributive laws involving * and -
1999-06-23, by paulson
rewrite rules to distribute CONSTANT multiplication over sum and difference;
1999-06-23, by paulson
another snapshot, still not working
1999-06-17, by paulson
new results about SKIP
1999-06-17, by paulson
addition of drop_... operators with new results and simplification of old ones
1999-06-17, by paulson
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
1999-06-17, by paulson
many new guarantees laws
1999-06-17, by paulson
moved image_UNION to Fun/image_UN
1999-06-17, by paulson
expandshort
1999-06-17, by paulson
renamed UNION_... to UN_... (to fit the convention)
1999-06-17, by paulson
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
1999-06-17, by paulson
not working but taking shape
1999-06-13, by paulson
guar; locale for the spec
1999-06-13, by paulson
many new results for reachable and lift_prog
1999-06-13, by paulson
new finiteness theorems
1999-06-13, by paulson
renamed pfix_[lg}e
1999-06-13, by paulson
new-style infix directives
1999-06-13, by paulson
guarantees -> guar
1999-06-13, by paulson
guarantees -> juar
1999-06-13, by paulson
rev=rev lemma.
1999-06-11, by nipkow
fixed title line; added spacing
1999-06-11, by paulson
no longer needs ../Lex
1999-06-11, by paulson
new UNITY files
1999-06-11, by paulson
unclosed comment.
1999-06-10, by nipkow
The Allocator example: specifications
1999-06-10, by paulson
expandshort
1999-06-10, by paulson
many new lemmas about take & drop, incl the famous take-lemma
1999-06-10, by paulson
moved predicates refl, sym down to Relation.thy
1999-06-10, by paulson
Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra
1999-06-10, by paulson
using the new GenPrefix theory
1999-06-10, by paulson
shortened Follows to Fols
1999-06-10, by paulson
tidied
1999-06-10, by paulson
new translation to allow images over Nonce
1999-06-10, by paulson
new preficates refl, sym [from Integ/Equiv], antisym
1999-06-10, by paulson
new lemma less_Suc_eq_0_disj
1999-06-10, by paulson
Generalized prefix theory, replacing the reference to directory Lex.
1999-06-10, by paulson
Stefan Merz's lemmas.
1999-06-09, by nipkow
added square root example.
1999-06-08, by nipkow
renamed the underlying relation of leadsTo from "leadsto"
1999-06-08, by paulson
removed obsolete "Prefix" ancestor
1999-06-08, by paulson
new classical example from Lewis Carroll via S G Pulman
1999-06-08, by paulson
tuned mode_name;
1999-06-07, by wenzelm
improved handling of assumptions;
1999-06-07, by wenzelm
facts: bind named props (from proof.ML/let_thms);
1999-06-07, by wenzelm
reset HOL_quantifiers by default;
1999-06-07, by wenzelm
Added lots of 'replicate' lemmas.
1999-06-07, by nipkow
groups as monoids;
1999-06-05, by wenzelm
tuned comments;
1999-06-05, by wenzelm
added Ord.order_antisym;
1999-06-05, by wenzelm
auto_bind_goal, auto_bind_facts;
1999-06-05, by wenzelm
auto_bind_goal, auto_bind_facts;
1999-06-05, by wenzelm
added get_st;
1999-06-05, by wenzelm
tuned;
1999-06-05, by wenzelm
varifyT': observe additional 'fixed' tfrees;
1999-06-05, by wenzelm
removed ObjectLogic.setup;
1999-06-05, by wenzelm
proper calculation;
1999-06-05, by wenzelm
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
1999-06-05, by wenzelm
fixed "...": dest_arg;
1999-06-04, by wenzelm
oops;
1999-06-04, by wenzelm
added order_le_less_trans, order_less_le_trans;
1999-06-04, by wenzelm
Calculation.thy: Setup transitivity rules for calculational proofs.
1999-06-04, by wenzelm
Support for calculational proofs.
1999-06-04, by wenzelm
added put_st;
1999-06-04, by wenzelm
added the_fact, level;
1999-06-04, by wenzelm
export multi_resolve;
1999-06-04, by wenzelm
added also, finally;
1999-06-04, by wenzelm
added 'also', 'finally' commands;
1999-06-04, by wenzelm
added COMP attribute;
1999-06-04, by wenzelm
added calculation.ML;
1999-06-04, by wenzelm
added Isar/calculation.ML;
1999-06-04, by wenzelm
fixed BUG in have_thmss: return thy';
1999-06-04, by wenzelm
added dest_main_statement;
1999-06-04, by wenzelm
print "..." variable;
1999-06-04, by wenzelm
no message "Adding axioms for datatype(s)";
1999-06-04, by wenzelm
added Group.thy;
1999-06-04, by wenzelm
added Isar_examples/Group.thy;
1999-06-04, by wenzelm
Some bits of group theory. Demonstrate calculational proofs.
1999-06-04, by wenzelm
read_term/prop_pat: do not freeze;
1999-06-02, by wenzelm
added dddot_tr;
1999-06-02, by wenzelm
added dddot_indexname;
1999-06-02, by wenzelm
"..." syntax;
1999-06-02, by wenzelm
find -print;
1999-06-02, by wenzelm
'kill' made improper;
1999-06-01, by wenzelm
improved print_state;
1999-06-01, by wenzelm
'note': Toplevel.print;
1999-06-01, by wenzelm
tuned markup;
1999-06-01, by wenzelm
broder size 3;
1999-06-01, by wenzelm
setup_goal: proper handling of non-atomic goals (include cprems into asms);
1999-05-31, by wenzelm
Isabelle manuals now also available as PDF;
1999-05-31, by wenzelm
move pdfs back into dist;
1999-05-28, by wenzelm
pdf docs;
1999-05-28, by wenzelm
separate archive for pdf docs;
1999-05-28, by wenzelm
\def\bold;
1999-05-28, by wenzelm
tuned formal comments;
1999-05-28, by wenzelm
tuned manual.bib;
1999-05-28, by wenzelm
changed {| |} verbatim syntax to {* *};
1999-05-27, by wenzelm
changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;
1999-05-27, by wenzelm
improved undo / kill operations;
1999-05-27, by wenzelm
fixed corruptoin of end of file
1999-05-27, by paulson
removal of Always_StableI
1999-05-27, by paulson
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
1999-05-27, by paulson
component_eq_subset: a neat characterization of "component"
1999-05-27, by paulson
ex/Points Isar'ized;
1999-05-26, by wenzelm
local_qed: print_result;
1999-05-26, by wenzelm
cannot_undo;
1999-05-26, by wenzelm
cannot_undo;
1999-05-26, by wenzelm
qed_block keywords;
1999-05-26, by wenzelm
local qeds: pass cond_print_result;
1999-05-26, by wenzelm
cleaned comments;
1999-05-26, by wenzelm
new theories Follows and ListOrder
1999-05-26, by paulson
formal comments (still dummy);
1999-05-25, by wenzelm
added formal comment arguments almost everywhere (still ignored);
1999-05-25, by wenzelm
renamed Comment.empty to Comment.none;
1999-05-25, by wenzelm
renamed Comment.empty to Comment.none;
1999-05-25, by wenzelm
renamed empty to none;
1999-05-25, by wenzelm
fixed cvs Id;
1999-05-25, by wenzelm
outer syntax keyword classification;
1999-05-24, by wenzelm
added keyword classification;
1999-05-24, by wenzelm
tuned print_context;
1999-05-24, by wenzelm
write_keywords generates outer syntax keyword classification in elisp;
1999-05-24, by wenzelm
outer syntax keyword classification;
1999-05-24, by wenzelm
renamed Lprg to Lift; simplified proof of Always_nonneg
1999-05-24, by paulson
int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
1999-05-24, by paulson
Better simplification of (nat #0), (int (Suc 0)), etc
1999-05-24, by paulson
UN_singleton->UN_constant_eq removes clash with other UN_singleton
1999-05-24, by paulson
new rule single_leadsTo_I; stronger PSP rule
1999-05-24, by paulson
increasing makes sense only for partial orderings
1999-05-24, by paulson
generalized increasing_size to mono_increasing_o
1999-05-24, by paulson
updated for stronger version of psp
1999-05-24, by paulson
new rule single_LeadsTo_I; stronger PSP rule; PSP_stable2->PSP_Stable2
1999-05-24, by paulson
expandshort
1999-05-24, by paulson
lists are partially ordered by the prefix relation
1999-05-24, by paulson
using generic rules when possible
1999-05-24, by paulson
Theory of the "Follows" relation
1999-05-24, by paulson
Increasing makes sense only for partial orderings
1999-05-24, by paulson
generalized Increasing_size to mono_Increasing_o
1999-05-24, by paulson
tidied
1999-05-24, by paulson
renamed PSP_stable2->PSP_Stable2
1999-05-24, by paulson
now uses mono_Increasing_o
1999-05-24, by paulson
updated for stronger version of psp
1999-05-24, by paulson
Configuration for ProofGeneral of LFCS Edinburgh.
1999-05-21, by wenzelm
Configuration for David Aspinall's Isamode.
1999-05-21, by wenzelm
Miscellaneous interfaces.
1999-05-21, by wenzelm
Isamode.setup, ProofGeneral.setup;
1999-05-21, by wenzelm
Isamode and ProofGeneral configuration moved to Pure/Interface;
1999-05-21, by wenzelm
added use_thy_only;
1999-05-21, by wenzelm
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
1999-05-21, by wenzelm
avoid string constants;
1999-05-21, by wenzelm
qed indexed.
1999-05-21, by nipkow
typedef_proof: pass interactive flag;
1999-05-21, by wenzelm
tuned;
1999-05-21, by wenzelm
cleaned comments;
1999-05-21, by wenzelm
renamed 'begin' / 'end' to '{{' / '}}';
1999-05-21, by wenzelm
history commands;
1999-05-21, by wenzelm
tuned;
1999-05-21, by wenzelm
adapted to History changes;
1999-05-21, by wenzelm
local_qed: obtain interactive flag;
1999-05-21, by wenzelm
backup replaced by checkpoint;
1999-05-21, by wenzelm
added default_prompt;
1999-05-21, by wenzelm
optional limit;
1999-05-21, by wenzelm
improved errors;
1999-05-21, by wenzelm
updated comment
1999-05-21, by paulson
made definition more readable
1999-05-21, by paulson
preferring generic rules to specific ones...
1999-05-21, by paulson
changes to show that Lists are partially ordered by the prefix relation
1999-05-21, by paulson
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)
1999-05-21, by paulson
redid proofs to use "always" rather than "reachable" (somewhat)
1999-05-19, by paulson
new theorem Always_reachable
1999-05-19, by paulson
tuned;
1999-05-18, by wenzelm
added Locale paper
1999-05-18, by paulson
locale documentation (from Florian)
1999-05-18, by paulson
../manual.bib a new dependency
1999-05-18, by paulson
cleaned comments;
1999-05-17, by wenzelm
cleaned comments;
1999-05-17, by wenzelm
tuned;
1999-05-17, by wenzelm
cleaned comments;
1999-05-17, by wenzelm
ThyInfo.finalize_all renamed to ThyInfo.finish;
1999-05-17, by wenzelm
node_cases renamed to node_case;
1999-05-17, by wenzelm
prep_ext exported (again);
1999-05-17, by wenzelm
backup operation replaces transaction;
1999-05-17, by wenzelm
removed get_nodes;
1999-05-17, by wenzelm
remove_thy;
1999-05-17, by wenzelm
tuned arrows;
1999-05-17, by wenzelm
Arrows are no longer needed because of redesign of the
1999-05-17, by berghofe
Changed some file names.
1999-05-17, by berghofe
Added function get_preds.
1999-05-17, by berghofe
Added setup for BrowserInfo.
1999-05-17, by berghofe
usedir now recognizes additional option -P which is used to
1999-05-17, by berghofe
Changed interface of function use_dir.
1999-05-17, by berghofe
Present.begin_theory now needs an additional argument of type
1999-05-17, by berghofe
Reimplemented graph generator.
1999-05-17, by berghofe
Added some code to enable browser to display remote documents.
1999-05-17, by berghofe
new thm extend_JN; renamed extend_leadsto
1999-05-17, by paulson
"component" now an infix
1999-05-17, by paulson
indentation
1999-05-17, by paulson
tuned;
1999-05-15, by wenzelm
ad-hoc fix for bold indexes;
1999-05-12, by wenzelm
strip_quotes replaced by unenclose;
1999-05-12, by wenzelm
rearranged some modules;
1999-05-12, by wenzelm
rearranged order of modules;
1999-05-12, by wenzelm
Basic URLs.
1999-05-12, by wenzelm
added url.ML;
1999-05-12, by wenzelm
pdf setup;
1999-05-12, by wenzelm
tuned;
1999-05-12, by wenzelm
fixed msg;
1999-05-11, by wenzelm
moved scan.ML;
1999-05-11, by wenzelm
new comments, variable renaming, etc
1999-05-11, by paulson
tidied
1999-05-11, by paulson
changes for new manual.bib
1999-05-11, by paulson
make pdf;
1999-05-10, by wenzelm
tuned;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
cite HOLCF;
1999-05-10, by wenzelm
tuned;
1999-05-10, by wenzelm
axclass;
1999-05-10, by wenzelm
axclass;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
*** empty log message ***
1999-05-10, by wenzelm
*** empty log message ***
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
fixed URLs;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
replaced png by pdf;
1999-05-07, by wenzelm
pdf pics;
1999-05-07, by wenzelm
tidied
1999-05-07, by paulson
tidied
1999-05-07, by paulson
new refererences for Inductive manual, but still incomplete
1999-05-07, by paulson
tuned;
1999-05-06, by wenzelm
pdf setup;
1999-05-06, by wenzelm
*** empty log message ***
1999-05-06, by wenzelm
pdf setup;
1999-05-06, by wenzelm
tuned;
1999-05-06, by wenzelm
More refs.
1999-05-06, by nipkow
Refs.
1999-05-06, by nipkow
New title page.
1999-05-06, by nipkow
tuned;
1999-05-05, by wenzelm
manual.bib;
1999-05-05, by wenzelm
no rail;
1999-05-05, by wenzelm
fixed FILES;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
isabelle.eps;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
tuned;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
*** empty log message ***
1999-05-05, by wenzelm
Common part for Doc Makefiles;
1999-05-05, by wenzelm
Now uses manual.bib; some references updated
1999-05-05, by paulson
tuned rpm file names;
1999-05-05, by wenzelm
updated docs;
1999-05-05, by wenzelm
Bibtex database for documentation.
1999-05-05, by nipkow
Bibtex stuff.
1999-05-05, by nipkow
*** empty log message ***
1999-05-04, by wenzelm
HOL;
1999-05-04, by wenzelm
removed HOL.tex;
1999-05-04, by wenzelm
tuned;
1999-05-04, by wenzelm
updated;
1999-05-04, by wenzelm
HOL part moved to 'logics-HOL' manual;
1999-05-04, by wenzelm
fixed;
1999-05-04, by wenzelm
used to be part of 'logics' manual;
1999-05-04, by wenzelm
isabelle_zf image;
1999-05-04, by wenzelm
*** empty log message ***
1999-05-04, by wenzelm
Arithmetic.
1999-05-04, by nipkow
add_recdef: removed names / attributes;
1999-05-04, by wenzelm
new definitions of Co and LeadsTo
1999-05-04, by paulson
transaction: Theory.copy;
1999-05-04, by wenzelm
hide prep_ext, merge_theories;
1999-05-04, by wenzelm
oops;
1999-05-04, by wenzelm
tuned;
1999-05-04, by wenzelm
Invariant -> Always and other tidying
1999-05-04, by paulson
tuned;
1999-05-03, by wenzelm
theory loader stuff updated and improved;
1999-05-03, by wenzelm
fixed reqs?
1999-05-03, by wenzelm
improved error handling
1999-05-03, by paulson
renamed state variables
1999-05-03, by paulson
tidied
1999-05-03, by paulson
tuned;
1999-05-03, by wenzelm
prefer /bin for ./configure;
1999-05-03, by wenzelm
try chown root:root;
1999-05-03, by wenzelm
renamed 'dummy' to 'dummy_pattern' (less dangerous);
1999-05-01, by wenzelm
tuned;
1999-04-30, by wenzelm
method = meth3 (again);
1999-04-30, by wenzelm
peoper defer_recdef interface;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
separated recdef / defer_recdef;
1999-04-30, by wenzelm
tuned defer_recdef interfaces;
1999-04-30, by wenzelm
comment, interest;
1999-04-30, by wenzelm
Comment.text;
1999-04-30, by wenzelm
comment sections;
1999-04-30, by wenzelm
dummy patterns;
1999-04-30, by wenzelm
added Isar/comment.ML;
1999-04-30, by wenzelm
val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
improved icons;
1999-04-30, by wenzelm
Isabelle icons;
1999-04-30, by wenzelm
patched sum_case;
1999-04-30, by wenzelm
Obsolete because JDK 1.1.x contains a class ScrollPane
1999-04-29, by berghofe
Updated to JDK 1.1.x
1999-04-29, by berghofe
Proof mods due to eta contraction during rewriting.
1999-04-29, by nipkow
Eta contraction is now performed all the time during rewriting.
1999-04-29, by nipkow
currently disabled;
1999-04-29, by wenzelm
*** empty log message ***
1999-04-29, by wenzelm
made many specification operators infix
1999-04-29, by paulson
eliminated theory UNITY/Traces
1999-04-28, by paulson
improper simp methods;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
fold / unfold methods;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
no Toplevel.print for by, ., ..;
1999-04-27, by wenzelm
improved print_state;
1999-04-27, by wenzelm
verbose flag;
1999-04-27, by wenzelm
use_thy_only made pervasive;
1999-04-27, by wenzelm
added Isar_examples/NatSum.thy;
1999-04-27, by wenzelm
Old stuff.
1999-04-27, by nipkow
proper quiet_mode;
1999-04-27, by wenzelm
adapted add_inductive, add_record;
1999-04-27, by wenzelm
adapted add_inductive;
1999-04-27, by wenzelm
intrs attributes;
1999-04-27, by wenzelm
proper quiet_mode;
1999-04-27, by wenzelm
iff_add_global (from simpdata.ML);
1999-04-27, by wenzelm
support forward chaining;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
added Isar_examples/Cantor.ML;
1999-04-27, by wenzelm
hol_setup, simpdata_setup;
1999-04-27, by wenzelm
"iff" attribute;
1999-04-27, by wenzelm
hol_setup;
1999-04-27, by wenzelm
"!" made keyword;
1999-04-27, by wenzelm
opt_thm_name: name optional;
1999-04-27, by wenzelm
added oooo;
1999-04-27, by wenzelm
fixed a bug many years old in rule plusEC
1999-04-26, by paulson
tuned msgs;
1999-04-26, by wenzelm
tuned;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
elaborated;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
tuned antiquotations;
1999-04-23, by wenzelm
improved 'single' method;
1999-04-23, by wenzelm
added thus, hence;
1999-04-23, by wenzelm
added FINISHED, same_tac;
1999-04-23, by wenzelm
use /usr/share and /usr/bin;
1999-04-23, by wenzelm
Now for recdefs that omit the WF relation;
1999-04-23, by paulson
Now for recdefs that omit the WF relation
1999-04-23, by paulson
Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml
1999-04-23, by paulson
chgrp isabelle;
1999-04-23, by wenzelm
detailed proofs;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
oops;
1999-04-23, by wenzelm
fixed IO;
1999-04-22, by wenzelm
improved load paths;
1999-04-22, by wenzelm
single method: include not_elim, imp_elim;
1999-04-22, by wenzelm
more graceful handling of load paths;
1999-04-22, by wenzelm
improved auto dir handling;
1999-04-22, by wenzelm
tuned;
1999-04-22, by wenzelm
make Isabelle rpm packages for Linux/x86 from the distribution;
1999-04-22, by wenzelm
use_thy etc.: may specify path prefix, which is temporarily used as load path;
1999-04-22, by wenzelm
switch_theory: Context.pass;
1999-04-22, by wenzelm
recdef (TFL) now requires theory Recdef;
1999-04-22, by wenzelm
recdef requires theory Recdef;
1999-04-22, by wenzelm
tuned;
1999-04-22, by wenzelm
rep_datatype syntax: 'induction' instead of 'induct';
1999-04-22, by wenzelm
add_recdef: actual simpset;
1999-04-22, by wenzelm
recdef adapted to RecdefPackage.add_recdef;
1999-04-22, by wenzelm
Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML;
1999-04-22, by wenzelm
added ex and Modelcheck
1999-04-22, by mueller
tuned;
1999-04-22, by wenzelm
added for mucke translation;
1999-04-22, by mueller
deleted some old examples in Modelcheck;
1999-04-22, by mueller
added translation from IOA to mucalculus and corresponding modelchecker examples;
1999-04-22, by mueller
moved this trivial example to new ex dir;
1999-04-22, by mueller
changed to include new subdirs ex and Modelcheck;
1999-04-22, by mueller
put types into "" because of signature clash;
1999-04-22, by mueller
added frontend syntax for IOA, moved trivial examples to folder ex;
1999-04-22, by mueller
added modelchecker mucke besides modelchecker eindhoven;
1999-04-22, by mueller
delete old files for adding second modelchecker connection;
1999-04-22, by mueller
$ML_HOME/.arch-n-opsys 2>/dev/null;
1999-04-21, by wenzelm
smlnj-110 setup made default;
1999-04-21, by wenzelm
/usr/share/smlnj/bin;
1999-04-21, by wenzelm
Isamode 2.6 requires patch;
1999-04-21, by wenzelm
added is_current;
1999-04-21, by wenzelm
fixed ISABELLE_HOME/lib/logo/isabelle-tiny.xpm;
1999-04-20, by wenzelm
temporarily fake quiet_mode;
1999-04-20, by wenzelm
temporarily reverted to 1.24;
1999-04-20, by wenzelm
IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly)
1999-04-20, by paulson
Main is the correct parent
1999-04-20, by paulson
new result extend_LeadsTo
1999-04-20, by paulson
should not refer to Datatype
1999-04-20, by paulson
addition of Kerberos IV example
1999-04-20, by paulson
tidied
1999-04-20, by paulson
improved usage;
1999-04-19, by wenzelm
loadpath replaced;
1999-04-16, by wenzelm
and_list;
1999-04-16, by wenzelm
lifted enum;
1999-04-16, by wenzelm
may specify induction predicates as well;
1999-04-16, by wenzelm
added Isar_examples;
1999-04-16, by wenzelm
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
1999-04-16, by wenzelm
lemmas about proper subset relation;
1999-04-16, by wenzelm
Proof by induction on types / set / functions.
1999-04-16, by wenzelm
print_datatypes;
1999-04-16, by wenzelm
added Tools/induct_method.ML;
1999-04-16, by wenzelm
'HOL/recdef' theory data;
1999-04-16, by wenzelm
'HOL/recdef' theory data;
1999-04-16, by wenzelm
'HOL/inductive' theory data;
1999-04-16, by wenzelm
Sign.base_name fid;
1999-04-16, by wenzelm
added incr_indexes, incr_indexes_wrt;
1999-04-16, by wenzelm
Proof mod.
1999-04-15, by nipkow
Added new thms.
1999-04-15, by nipkow
quiet_mode;
1999-04-14, by wenzelm
Tools/inductive_package.ML;
1999-04-14, by wenzelm
triple_swap;
1999-04-14, by wenzelm
Wrapper module for Konrad Slind's TFL package.
1999-04-14, by wenzelm
remoced old set_current_thy;
1999-04-14, by wenzelm
tuned messages;
1999-04-14, by wenzelm
intrs: names and atts;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
intrs: provide names and atts;
1999-04-14, by wenzelm
cleaned comments;
1999-04-14, by wenzelm
tuned;
1999-04-14, by wenzelm
fixed named type infixes (actual BUG!);
1999-04-14, by wenzelm
updated isatool install;
1999-04-13, by wenzelm
-p option;
1999-04-13, by wenzelm
adapted isatool install;
1999-04-13, by wenzelm
improved isatool install;
1999-04-13, by wenzelm
tuned;
1999-04-13, by wenzelm
ML_PLATFORM;
1999-04-12, by wenzelm
ML_PLATFORM;
1999-04-12, by wenzelm
fixed @@;
1999-04-07, by wenzelm
fixed bib file
1999-04-04, by paulson
fixed;
1999-04-03, by wenzelm
new definition for nth.
1999-04-01, by pusch
useless relic
1999-03-31, by nipkow
arith_tac
1999-03-30, by nipkow
tuned;
1999-03-19, by wenzelm
common qed and end of proofs;
1999-03-19, by wenzelm
* New bounded quantifier syntax (input only):
1999-03-18, by nipkow
New bounded quantifier syntax: !x<i. P etc
1999-03-18, by nipkow
added new theory Yahalom_Bad
1999-03-18, by paulson
added new theory Yahalom_Bad
1999-03-18, by paulson
exchanged the order of Gets and Notes in datatype event
1999-03-18, by paulson
fixed thm_name again;
1999-03-17, by wenzelm
Theory.sign_of;
1999-03-17, by wenzelm
xnum token class;
1999-03-17, by wenzelm
xstr token class;
1999-03-17, by wenzelm
Theory.sign_of;
1999-03-17, by wenzelm
fixed axclass_tac;
1999-03-17, by wenzelm
tuned;
1999-03-17, by wenzelm
Theory.sign_of;
1999-03-17, by wenzelm
qualify Theory.sign_of etc.;
1999-03-17, by wenzelm
fixed msg;
1999-03-17, by wenzelm
tuned msg;
1999-03-17, by wenzelm
axclass_tac lost an argument;
1999-03-17, by wenzelm
HOL/typedef: fixed type inference for representing set;
1999-03-17, by wenzelm
rep_datatype: '_i' version, attributes, outer syntax;
1999-03-17, by wenzelm
local open OuterParse;
1999-03-17, by wenzelm
actually check non-emptiness theorem;
1999-03-17, by wenzelm
fixed typedef representing set;
1999-03-17, by wenzelm
adapted rep_datatype;
1999-03-17, by wenzelm
added dest_mem;
1999-03-17, by wenzelm
theory data;
1999-03-17, by wenzelm
adapted AxClass.add_axclass;
1999-03-17, by wenzelm
tuned msgs;
1999-03-17, by wenzelm
tuned;
1999-03-17, by wenzelm
cleaned comments;
1999-03-17, by wenzelm
added apply_cond_open;
1999-03-17, by wenzelm
added (improper_)command;
1999-03-17, by wenzelm
added simple_arity, spec_name, spec_opt_name;
1999-03-17, by wenzelm
added '_i' versions;
1999-03-17, by wenzelm
OuterSyntax.(improper_)command;
1999-03-17, by wenzelm
added assert_super;
1999-03-17, by wenzelm
added def_name;
1999-03-17, by wenzelm
added cond_extern_thm_sg;
1999-03-17, by wenzelm
AxClass.setup;
1999-03-17, by wenzelm
axclass.ML loaded after Isar;
1999-03-17, by wenzelm
made weblint happy;
1999-03-12, by wenzelm
comment;
1999-03-12, by wenzelm
removed obsolete user data stuff;
1999-03-12, by wenzelm
theory: include parent links;
1999-03-12, by wenzelm
outer syntax for 'datatype';
1999-03-11, by wenzelm
add_primrec(_i): attributes;
1999-03-11, by wenzelm
outer syntax for 'record';
1999-03-11, by wenzelm
named witnesses: PureThy.get_thmss;
1999-03-11, by wenzelm
primrec: empty attributes;
1999-03-11, by wenzelm
tuned opt_mixfix failure;
1999-03-11, by wenzelm
add_title;
1999-03-11, by wenzelm
added 'title';
1999-03-11, by wenzelm
tuned space;
1999-03-11, by wenzelm
comment;
1999-03-11, by wenzelm
workaround default_name problem;
1999-03-11, by wenzelm
removed foo_build_completed -- now handled by session management (via usedir);
1999-03-11, by wenzelm
include 'README';
1999-03-11, by wenzelm
tuned;
1999-03-11, by wenzelm
moved Thy/session.ML to Isar/session.ML;
1999-03-11, by wenzelm
tuned;
1999-03-10, by wenzelm
-x option;
1999-03-10, by wenzelm
updated;
1999-03-10, by wenzelm
report session path;
1999-03-10, by wenzelm
report path instead of actual session;
1999-03-10, by wenzelm
HTML output;
1999-03-10, by wenzelm
maintain current/parent index;
1999-03-10, by wenzelm
output: some symbol translations;
1999-03-10, by wenzelm
parent_session;
1999-03-10, by wenzelm
allow meta_outer to do nothing
1999-03-10, by paulson
updating both Yahalom protocols to the Gets model
1999-03-10, by paulson
updated not_bad_tac for the Gets model
1999-03-10, by paulson
deleted obsolete comments
1999-03-10, by paulson
Present.theory_source;
1999-03-09, by wenzelm
begin/end_theory: presentation;
1999-03-09, by wenzelm
checkpoint -- basic functionality only;
1999-03-09, by wenzelm
added use_path;
1999-03-09, by wenzelm
IsarThy.begin/end_theory;
1999-03-09, by wenzelm
Present.theorem;
1999-03-09, by wenzelm
fixed add_path reset;
1999-03-09, by wenzelm
still fake, passes BrowserInfo;
1999-03-09, by wenzelm
HTML markup elements.
1999-03-09, by wenzelm
added html.ML, browser_info.ML;
1999-03-09, by wenzelm
token translation: real;
1999-03-09, by wenzelm
added strlen_real, setmp_margin;
1999-03-09, by wenzelm
tuned using nth_elem_string, exists_string;
1999-03-09, by wenzelm
added make, dir;
1999-03-09, by wenzelm
added mkdir;
1999-03-09, by wenzelm
added Buffer;
1999-03-09, by wenzelm
simple string buffers;
1999-03-09, by wenzelm
*** empty log message ***
1999-03-09, by wenzelm
pretty_thm_no_quote;
1999-03-09, by wenzelm
HTML.setup;
1999-03-09, by wenzelm
added nth_elem_string, exists_string;
1999-03-09, by wenzelm
token translation: real;
1999-03-09, by wenzelm
tuned;
1999-03-09, by wenzelm
tidied
1999-03-09, by paulson
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
1999-03-09, by paulson
Suc -> +1
1999-03-08, by nipkow
modified zip
1999-03-08, by nipkow
Fixed bug in add_datatype_axm:
1999-03-05, by berghofe
fixed again;
1999-03-04, by wenzelm
expandshort
1999-03-03, by paulson
added UNITY/Extend
1999-03-03, by paulson
expandshort
1999-03-03, by paulson
tidied
1999-03-03, by paulson
UNITY fully working at last...
1999-03-03, by paulson
expandshort
1999-03-03, by paulson
new theory of extending the state space
1999-03-03, by paulson
fixed {ISABELLE};
1999-03-01, by wenzelm
removed the infernal States, eqStates, compatible, etc.
1999-03-01, by paulson
tidied
1999-03-01, by paulson
simpler proofs of congruence rules
1999-03-01, by paulson
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
1999-03-01, by paulson
simpler proofs of congruence rules
1999-03-01, by paulson
new image laws
1999-02-22, by paulson
added a commment on the "ext" rule
1999-02-22, by paulson
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
1999-02-22, by paulson
added rev_bexI
1999-02-22, by paulson
fixed order of multiple -m options;
1999-02-18, by wenzelm
fixed geometry;
1999-02-18, by grobauer
tidying in conjuntion with the TISSEC paper; replaced (unit option)
1999-02-16, by paulson
new theorem image_Union_eq
1999-02-16, by paulson
foldl_string;
1999-02-13, by wenzelm
renamed space2 to spacespace
1999-02-12, by oheimb
tuned pretty format lookup;
1999-02-12, by wenzelm
pretty_thm: quote terms (separately);
1999-02-12, by wenzelm
Symbol.output subject to print mode;
1999-02-11, by wenzelm
-m isabelle_font;
1999-02-11, by wenzelm
tuned;
1999-02-11, by wenzelm
Present.init;
1999-02-11, by wenzelm
init, finish;
1999-02-11, by wenzelm
proper handling of print_mode wrt. Pretty.sym;
1999-02-11, by wenzelm
added output_width;
1999-02-11, by wenzelm
sym: Symbol.output_width;
1999-02-11, by wenzelm
val appends: T list -> T;
1999-02-11, by wenzelm
tuned;
1999-02-11, by wenzelm
tidied; better error messages
1999-02-09, by paulson
new lemma surjD
1999-02-09, by paulson
Context.fetch, Context.setmp;
1999-02-08, by wenzelm
"files" keyword!
1999-02-08, by wenzelm
use: provide context;
1999-02-08, by wenzelm
tuned msgs;
1999-02-08, by wenzelm
tuned msg;
1999-02-08, by wenzelm
added fetch, fetch_theory;
1999-02-08, by wenzelm
~~;
1999-02-08, by wenzelm
path element specification '~~' refers to '$ISABELLE_HOME';
1999-02-08, by wenzelm
no deps on compile time sources;
1999-02-08, by wenzelm
isatool logo;
1999-02-08, by wenzelm
-i option;
1999-02-08, by wenzelm
updated (Stephan Merz);
1999-02-08, by wenzelm
updated TLA;
1999-02-08, by wenzelm
made MLWorks happy;
1999-02-05, by wenzelm
examples made separate dirs;
1999-02-05, by wenzelm
add_path;
1999-02-05, by wenzelm
Hyperreal made part of Real;
1999-02-05, by wenzelm
Session.use_dir: check parent;
1999-02-05, by wenzelm
*** empty log message ***
1999-02-05, by wenzelm
more robust handling of theory context;
1999-02-05, by wenzelm
improved theory, context, update_context;
1999-02-05, by wenzelm
improved 'theory';
1999-02-05, by wenzelm
improved msg;
1999-02-05, by wenzelm
use_thy, update_thy: Context.save;
1999-02-05, by wenzelm
tuned;
1999-02-05, by wenzelm
time_use made pervasive;
1999-02-05, by wenzelm
use_dir: check parent, more robust exit;
1999-02-05, by wenzelm
more robust RC;
1999-02-05, by wenzelm
setmp: theory option;
1999-02-05, by wenzelm
Session.finish ();
1999-02-05, by wenzelm
tidied Schroeder-Bernstein proof
1999-02-05, by paulson
new surj rules
1999-02-05, by paulson
obsolete;
1999-02-04, by wenzelm
tuned;
1999-02-04, by wenzelm
include full paths in file info;
1999-02-04, by wenzelm
Symbol.use;
1999-02-04, by wenzelm
Symbol.use (eliminated Use.exit_use);
1999-02-04, by wenzelm
leave theory context after load_thy;
1999-02-04, by wenzelm
File.pwd, File.cd;
1999-02-04, by wenzelm
fixed file_info;
1999-02-04, by wenzelm
use, cd;
1999-02-04, by wenzelm
added 'use';
1999-02-04, by wenzelm
fail_safe close;
1999-02-04, by wenzelm
check_elem: allow ~, except for '~' and '~~';
1999-02-04, by wenzelm
removed use.ML;
1999-02-04, by wenzelm
removed General/use.ML;
1999-02-04, by wenzelm
made SML/NJ happy;
1999-02-03, by wenzelm
check_thy: include ML stamp;
1999-02-03, by wenzelm
added join_info;
1999-02-03, by wenzelm
tidied load path handling;
1999-02-03, by wenzelm
add_path / reset_path;
1999-02-03, by wenzelm
tuned;
1999-02-03, by wenzelm
ThmDatabase.ml_store_thm;
1999-02-03, by wenzelm
usedir -r;
1999-02-03, by wenzelm
Session.init;
1999-02-03, by wenzelm
Theory loader database: theory and file dependencies, theory values
1999-02-03, by wenzelm
tidied;
1999-02-03, by wenzelm
Session management -- maintain state of logic images.
1999-02-03, by wenzelm
get_lexicon;
1999-02-03, by wenzelm
tokenize: get exploded args;
1999-02-03, by wenzelm
delete_tmpfiles (from thy_read.ML);
1999-02-03, by wenzelm
added reset_path;
1999-02-03, by wenzelm
open BasicThmDatabase;
1999-02-03, by wenzelm
Theory presentation (fake implementation);
1999-02-03, by wenzelm
moved to Pure/context.ML;
1999-02-03, by wenzelm
nuked;
1999-02-03, by wenzelm
moved to General/use.ML;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
ThyInfo.begin_theory;
1999-02-03, by wenzelm
oops, update_thy;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
comment;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
proper setup of preloaded theories (ThyInfo.register_theory);
1999-02-03, by wenzelm
renamed sig to PRIVATE_SIGN;
1999-02-03, by wenzelm
added thm, thms, Open_locale, Close_locale, Print_scope;
1999-02-03, by wenzelm
added Goal(w) and Export (from context.ML);
1999-02-03, by wenzelm
added is_draft;
1999-02-03, by wenzelm
enabled sig;
1999-02-03, by wenzelm
tuned msg;
1999-02-03, by wenzelm
Global theory context (used to be in Thy/context.ML);
1999-02-03, by wenzelm
moved several files;
1999-02-03, by wenzelm
more abstract implementation;
1999-02-03, by wenzelm
use Path.T;
1999-02-03, by wenzelm
of_file: Path.T, Position.T;
1999-02-03, by wenzelm
added use.ML;
1999-02-03, by wenzelm
added Use;
1999-02-03, by wenzelm
tuned;
1999-02-03, by wenzelm
tidied; added thy_load.ML
1999-02-03, by paulson
tidied, with left_inverse & right_inverse as default simprules
1999-02-03, by paulson
auto update
1999-02-03, by paulson
inj
1999-02-03, by paulson
documented typecheck_tac, etc
1999-02-03, by paulson
standard spelling: type-checking
1999-02-03, by paulson
inj is now a translation of inj_on
1999-02-03, by paulson
standard spelling: type-checking
1999-02-03, by paulson
a bit of tidying
1999-02-01, by paulson
Theory loader primitives.
1999-01-30, by wenzelm
corrected output of symbols for several (probably not all) relevant functions
1999-01-29, by oheimb
renamed space2 to spacespace
1999-01-29, by oheimb
corrected output of symbols for several (probably not all) relevant functions
1999-01-29, by oheimb
moved print_mode to ROOT.ML
1999-01-29, by oheimb
expandshort
1999-01-29, by paulson
expandshort
1999-01-29, by paulson
tidied
1999-01-29, by paulson
tidied
1999-01-28, by paulson
constdefs
1999-01-28, by paulson
tidying
1999-01-28, by paulson
arith_tac for min/max
1999-01-27, by nipkow
*** empty log message ***
1999-01-27, by wenzelm
ZF typechecking
1999-01-27, by paulson
automatic insertion of datatype intr rules into claset
1999-01-27, by paulson
new typechecking solver for the simplifier
1999-01-27, by paulson
tuned;
1999-01-25, by wenzelm
Fixed a bug in lin.arith.
1999-01-24, by nipkow
tuned;
1999-01-22, by wenzelm
tuned;
1999-01-22, by wenzelm
isabelle.in.tum.de;
1999-01-20, by wenzelm
http://isabelle.in.tum.de/dist/;
1999-01-20, by wenzelm
renamed variables for clarity
1999-01-20, by paulson
changed Minho mirror;
1999-01-20, by wenzelm
tidied freeness reasoning
1999-01-19, by paulson
freeness reasoning: T.free_iffs
1999-01-19, by paulson
tuned;
1999-01-19, by wenzelm
removal of the (thm list) argument of mk_cases
1999-01-19, by paulson
tidied; added dest_eq
1999-01-19, by paulson
simplified thanks to the arithmetic prover
1999-01-19, by paulson
updated comments
1999-01-19, by paulson
a simplification by G Bella
1999-01-19, by paulson
structure Graph = Graph;
1999-01-18, by wenzelm
GraphFun (generic directed graphs);
1999-01-18, by wenzelm
added General/graph.ML: generic direct graphs;
1999-01-18, by wenzelm
removed empty line (in case of empty begin_state marker) before Level line
1999-01-15, by oheimb
Removed superfluous arith rules from metric_simps
1999-01-14, by nipkow
More Arith.
1999-01-14, by nipkow
Fixed old bug: selection of constant to be split should depend not just on
1999-01-14, by nipkow
nat_arith_tac -> arith_tac
1999-01-14, by nipkow
More arith refinements.
1999-01-14, by nipkow
tuned README;
1999-01-14, by wenzelm
Pure/General/symbol.ML;
1999-01-14, by wenzelm
tuned;
1999-01-14, by wenzelm
deleted the appendices because documentation exists in the HOL and ZF manuals
1999-01-13, by paulson
defined dquotesoff
1999-01-13, by paulson
new manual ZF
1999-01-13, by paulson
the separate FOL and ZF logics manual, with new material on datatypes and
1999-01-13, by paulson
removal of FOL and ZF
1999-01-13, by paulson
minor updates on inductive definitions and datatypes
1999-01-13, by paulson
fixed titles;
1999-01-13, by wenzelm
tidying of datatype and inductive definitions
1999-01-13, by paulson
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
1999-01-13, by wenzelm
Refined arithmetic.
1999-01-13, by nipkow
congruence rules finally use == instead of = and <->
1999-01-13, by paulson
generalized qed_spec_mp code to work for ZF
1999-01-13, by paulson
datatype package improvements
1999-01-13, by paulson
better qed_spec_mp
1999-01-13, by paulson
Simplified interface.
1999-01-13, by nipkow
Simplified arithmetic.
1999-01-13, by nipkow
'same' method, 'immediate' proof;
1999-01-12, by wenzelm
tuned msg;
1999-01-12, by wenzelm
SYNC;
1999-01-12, by wenzelm
fixed again;
1999-01-12, by wenzelm
improved asm_finish;
1999-01-12, by wenzelm
get_tthms witness theorems;
1999-01-12, by wenzelm
Split argument structure.
1999-01-12, by nipkow
Restructured Arithmatic
1999-01-12, by nipkow
*** empty log message ***
1999-01-12, by nipkow
verbatim
1999-01-12, by nipkow
SYNC;
1999-01-12, by wenzelm
fixed deriv;
1999-01-12, by wenzelm
eliminated tthm type and Attribute structure;
1999-01-12, by wenzelm
tuned msg;
1999-01-12, by wenzelm
tuned signature;
1999-01-12, by wenzelm
eliminated global/local names;
1999-01-12, by wenzelm
eliminated tthm type and Attribute structure;
1999-01-12, by wenzelm
eliminated tthm type and Attribute structure;
1999-01-12, by wenzelm
eliminated Attribute structure;
1999-01-12, by wenzelm
signature BASIC_THM;
1999-01-12, by wenzelm
fixed AUTO_PERL;
1999-01-12, by wenzelm
show_tags;
1999-01-12, by wenzelm
added rule_attribute: ('a -> thm -> thm) -> 'a attribute;
1999-01-12, by wenzelm
Thm of string * tag list;
1999-01-12, by wenzelm
eliminated Attribute structure;
1999-01-12, by wenzelm
removed attribute.ML;
1999-01-12, by wenzelm
configure AUTO_BASH, AUTO_PERL;
1999-01-12, by wenzelm
Some simplifications.
1999-01-11, by nipkow
More arith simplifications
1999-01-11, by nipkow
More arith simplifications.
1999-01-11, by nipkow
more robust heap file detection;
1999-01-11, by wenzelm
tuned, updated;
1999-01-11, by wenzelm
tidying, e.g. from \\tt to \\texttt
1999-01-11, by paulson
Remoaved a few now redundant rewrite rules.
1999-01-09, by nipkow
Added simproc.
1999-01-09, by nipkow
Refined arith tactic.
1999-01-09, by nipkow
removal of FOL, ZF to a separate manual
1999-01-08, by paulson
removal of DO_GOAL
1999-01-08, by paulson
ZF: the natural numbers as a datatype
1999-01-07, by paulson
if-then-else syntax for ZF
1999-01-07, by paulson
if-then-else syntax for ZF
1999-01-07, by paulson
fixed commit spec;
1999-01-06, by wenzelm
Simplified proof.
1999-01-06, by nipkow
induct_tac and exhaust_tac
1999-01-06, by paulson
primrec, induct_tac
1999-01-06, by paulson
*** empty log message ***
1999-01-05, by nipkow
Small mods.
1999-01-05, by nipkow
1 proof now automatic.
1999-01-05, by nipkow
Instantiated lin.arith.
1999-01-05, by nipkow
In Main: moved Bin to the left to preserve the solver in its simpset.
1999-01-05, by nipkow
Shortened a proof.
1999-01-04, by nipkow
*** empty log message ***
1999-01-04, by nipkow
Version 1 of linear arithmetic for nat.
1999-01-04, by nipkow
Version 1.0 of linear nat arithmetic.
1999-01-04, by nipkow
added new arg for print_tac
1998-12-28, by paulson
new inductive, datatype and primrec packages, etc.
1998-12-28, by paulson
revised datatype definition package
1998-12-28, by paulson
revised inductive definition package
1998-12-28, by paulson
new primrec package
1998-12-28, by paulson
moved from ZF to new subdirectory Tools
1998-12-28, by paulson
new theorem update_type
1998-12-28, by paulson
converted to use new primrec section and update operator
1998-12-28, by paulson
converted to use new primrec section
1998-12-28, by paulson
fixed comment
1998-12-28, by paulson
Needs separate theory Primrec_defs due to new inductive defs package
1998-12-28, by paulson
more efficient strip_quotes using "substring"
1998-12-28, by paulson
Basis Library compatible substring oeration
1998-12-28, by paulson
Added a "message" argument to print_tac
1998-12-28, by paulson
comments
1998-12-28, by paulson
deleted "escape" and "trim"; Basis Library can do string escapes if necessary
1998-12-28, by paulson
String added to BasisLibrary
1998-12-28, by paulson
better indentation
1998-12-28, by paulson
fixed comments
1998-12-28, by paulson
replaced obsolete "trim" by "strip_quotes"
1998-12-28, by paulson
Link to HOLCF paper added.
1998-12-18, by nipkow
moved dest_Type to term.ML from HOL/Tools/primrec_package
1998-12-18, by paulson
moved dest_eq to hologic.ML and tidied
1998-12-18, by paulson
new function dest_eq
1998-12-18, by paulson
tuned mode_name;
1998-12-17, by wenzelm
bash -c :;
1998-12-17, by wenzelm
*** empty log message ***
1998-12-11, by oheimb
added new print_mode "xsymbols" for extended symbol support
1998-12-11, by oheimb
better representation of Sigma
1998-12-11, by oheimb
initisaterm now obsolete
1998-12-11, by oheimb
new Close_locale synatx
1998-12-11, by paulson
deleted unclosed comment
1998-12-11, by paulson
the + facility for locales, by Florian
1998-12-11, by paulson
new Close_locale synatx
1998-12-11, by paulson
towards handling sharing of variables
1998-12-07, by paulson
tidying
1998-12-07, by paulson
expandshort
1998-12-07, by paulson
better export for nested locales
1998-12-04, by paulson
new (and generalized) theorems about Sigma/Times
1998-12-04, by paulson
locales: assumes and defines may be empty
1998-12-04, by paulson
locales
1998-12-04, by paulson
and_list;
1998-12-03, by wenzelm
Addition of the States component; parts of Comp not working
1998-12-03, by paulson
tuned;
1998-12-02, by wenzelm
IOA-Storage: Memory storage case study.
1998-12-02, by wenzelm
Memory storage case study.
1998-12-02, by wenzelm
Memory storage case study from PhD p.240;
1998-12-02, by mueller
new theorem Pow_UNIV
1998-12-02, by paulson
new rule rev_bexI
1998-12-02, by paulson
new theorems Domain_Union, Range_Union
1998-12-02, by paulson
removed duplicate contrapos;
1998-12-01, by wenzelm
enum: !!! after seperator;
1998-12-01, by wenzelm
excursion: ERROR_MESSAGE;
1998-12-01, by wenzelm
qed: kind_name (again);
1998-12-01, by wenzelm
show_tags flag;
1998-12-01, by wenzelm
new theorem INT_Un
1998-12-01, by paulson
better version of Image_diag
1998-12-01, by paulson
tactical CHANGED now uses alpha-eta conversion, not alpha conversion
1998-11-30, by paulson
Renamed subset_Sigma_llist to subset_Times_llist
1998-11-30, by paulson
new theorems about diag
1998-11-30, by paulson
fixed declatation of patterns and skolem;
1998-11-29, by wenzelm
tuned print_state;
1998-11-29, by wenzelm
tuned welcome msg;
1998-11-29, by wenzelm
added restart;
1998-11-29, by wenzelm
added exception RESTART;
1998-11-29, by wenzelm
proof_general_trans (experimental);
1998-11-29, by wenzelm
replaced wakeup by decorate_prompt_fn;
1998-11-29, by wenzelm
eliminated "Trying to recover ..." msg;
1998-11-29, by wenzelm
added oct_char;
1998-11-29, by wenzelm
method brute_force = ALLGOALS force_tac;
1998-11-29, by wenzelm
*** empty log message ***
1998-11-27, by nipkow
At last: linear arithmetic for nat!
1998-11-27, by nipkow
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
1998-11-27, by nipkow
fixed a link
1998-11-27, by paulson
added Real/Hyperreal
1998-11-27, by paulson
Addition of Hyperreal theories Zorn and Filter
1998-11-27, by paulson
moved diag (diagonal relation) from Univ to Relation
1998-11-27, by paulson
tidied up list definitions, using type 'a option instead of
1998-11-26, by paulson
tuning to assimiliate it with PhD;
1998-11-26, by mueller
Added a general refutation tactic which works by putting things into nnf first.
1998-11-26, by nipkow
Added filter_prems_tac
1998-11-26, by nipkow
removed prs / prs_fn;
1998-11-25, by wenzelm
guarantees laws
1998-11-25, by paulson
simplified ensures_UNIV
1998-11-25, by paulson
new thms for invariant
1998-11-25, by paulson
new theorem program_equalityE
1998-11-25, by paulson
renamed vars
1998-11-25, by paulson
image_id in simpset
1998-11-25, by paulson
removed prs / prs_fn (broken, because it did not include \n in its
1998-11-25, by wenzelm
eliminated ISABELLE_INTERFACE_OPTIONS;
1998-11-25, by wenzelm
improved comment;
1998-11-25, by wenzelm
replaced prs by std_output;
1998-11-25, by wenzelm
replaced prs by writeln;
1998-11-25, by wenzelm
replaced prs by std_output / writeln;
1998-11-25, by wenzelm
comment parser;
1998-11-25, by wenzelm
add_text, add_chapter etc.: dummy;
1998-11-25, by wenzelm
chapter etc. headings;
1998-11-25, by wenzelm
tuned space;
1998-11-25, by wenzelm
replaced prs by writeln;
1998-11-25, by wenzelm
removed redirect_to_latex stuff;
1998-11-25, by wenzelm
Isar.main();
1998-11-24, by wenzelm
setup Blast.setup;
1998-11-24, by wenzelm
added commands;
1998-11-24, by wenzelm
added isar.ML;
1998-11-24, by wenzelm
Isabelle/Isar main interface.
1998-11-24, by wenzelm
fixed prefix_lines: *separate* by \n;
1998-11-24, by wenzelm
added Isar/isar.ML;
1998-11-24, by wenzelm
fixed links
1998-11-23, by paulson
print_state hook, obeys Goals.current_goals_markers by default;
1998-11-21, by wenzelm
print_state: use begin_goal from Goals.current_goals_markers;
1998-11-21, by wenzelm
added undos, redos;
1998-11-21, by wenzelm
tty: issue wakeup;
1998-11-21, by wenzelm
std_output, prefix_lines;
1998-11-21, by wenzelm
better miniscoping rules: the premise C~={} is not good
1998-11-20, by paulson
fixed method syntax;
1998-11-19, by wenzelm
break: exhibit state stack;
1998-11-19, by wenzelm
match_bind: 'as' patterns;
1998-11-19, by wenzelm
let: 'as' patterns;
1998-11-19, by wenzelm
match_bind(_i): 'as' patterns;
1998-11-19, by wenzelm
term_pat vs. prop_pat;
1998-11-19, by wenzelm
term_pat vs. prop_pat;
1998-11-19, by wenzelm
no warning for "it" theorems;
1998-11-19, by wenzelm
tidied
1998-11-18, by paulson
Finally removing "Compl" from HOL
1998-11-18, by paulson
exn_message FAIL;
1998-11-18, by wenzelm
blast: cla_method';
1998-11-18, by wenzelm
export simp_modifiers;
1998-11-18, by wenzelm
expoer cla_method('), cla_modifiers;
1998-11-18, by wenzelm
method setup;
1998-11-18, by wenzelm
tuned comments;
1998-11-18, by wenzelm
'prop', 'term', 'typ';
1998-11-18, by wenzelm
load;
1998-11-18, by wenzelm
export exn_message;
1998-11-18, by wenzelm
removed trace;
1998-11-18, by wenzelm
BREAK: include state;
1998-11-17, by wenzelm
have_tthms;
1998-11-17, by wenzelm
PureThy.default_name;
1998-11-17, by wenzelm
generalized (opt_)thm_name;
1998-11-17, by wenzelm
exception METHOD_FAIL;
1998-11-17, by wenzelm
added have_theorems, have_lemmas, have_facts;
1998-11-17, by wenzelm
added 'theorems', 'lemmas', 'note';
1998-11-17, by wenzelm
break: exhibit state;
1998-11-17, by wenzelm
exception ATTRIB_FAIL;
1998-11-17, by wenzelm
removed trace;
1998-11-17, by wenzelm
Symbol.space;
1998-11-17, by wenzelm
space;
1998-11-17, by wenzelm
val spc: int -> T;
1998-11-17, by wenzelm
added default_name;
1998-11-17, by wenzelm
Drule.rev_triv_goal;
1998-11-17, by wenzelm
Theory.apply replaced by Library.apply;
1998-11-17, by wenzelm
val apply: ('a -> 'a) list -> 'a -> 'a;
1998-11-17, by wenzelm
export vars_of and friends;
1998-11-17, by wenzelm
Pretty.spc;
1998-11-17, by wenzelm
added pretty_tthms, print_tthms;
1998-11-17, by wenzelm
new theory UNITY/PPROD
1998-11-17, by paulson
new theory PPROD
1998-11-16, by paulson
a faster proof
1998-11-16, by paulson
removed genelim.ML;
1998-11-16, by wenzelm
thm, thms;
1998-11-16, by wenzelm
added print_thm;
1998-11-16, by wenzelm
made SML/NJ happy;
1998-11-16, by wenzelm
added oo, ooo (*concatenation: 2 and 3 args*);
1998-11-16, by wenzelm
Attribute.tthms_of;
1998-11-16, by wenzelm
Attribute.tthms_of;
1998-11-16, by wenzelm
Attribute.thms_of;
1998-11-16, by wenzelm
Classical.setup, attrib_setup;
1998-11-16, by wenzelm
attrib_setup: rulify;
1998-11-16, by wenzelm
attrib_setup;
1998-11-16, by wenzelm
all modifiers turned into attributes;
1998-11-16, by wenzelm
tuned attribute names;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
tuned names;
1998-11-16, by wenzelm
renamed tac / etac to refine / then_refine;
1998-11-16, by wenzelm
add print_theorems;
1998-11-16, by wenzelm
add print_theorems;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
removed args, args1, thm_xname;
1998-11-16, by wenzelm
replaced is_symid by is_sid;
1998-11-16, by wenzelm
renamed init_context to init;
1998-11-16, by wenzelm
renamed init_context to init;
1998-11-16, by wenzelm
structure PureIsar;
1998-11-16, by wenzelm
removed lift_modifier;
1998-11-16, by wenzelm
Attribute.thms_of;
1998-11-16, by wenzelm
Scan.read;
1998-11-16, by wenzelm
added read;
1998-11-16, by wenzelm
tuned usage of read;
1998-11-16, by wenzelm
generalized JN_empty and added reachable_SKIP
1998-11-16, by paulson
removed the reference to mesontest2.ML, itself now deleted
1998-11-16, by paulson
moved some facts about Pi from ex/PiSets to Fun.ML
1998-11-16, by paulson
prefixed op;
1998-11-14, by wenzelm
Theory.copy;
1998-11-14, by wenzelm
val copy: theory -> theory;
1998-11-14, by wenzelm
added unless, first;
1998-11-14, by wenzelm
added read_nat;
1998-11-14, by wenzelm
not needed in distribution
1998-11-13, by paulson
needed tidying desperately
1998-11-13, by paulson
qualified the name "restrict" since Fun.restrict exists too
1998-11-13, by paulson
moved Pi and -> (renamed funcset) to Fun.thy
1998-11-13, by paulson
the type of @evalcn was wrong
1998-11-13, by paulson
moved UNION_o to Fun.ML, since Fun.thy is no longer a parent of equalities
1998-11-13, by paulson
no longer loads Fun so that the Fun proofs can use equalities.thy
1998-11-13, by paulson
the function space operator
1998-11-13, by paulson
New section on advanced datatypes.
1998-11-12, by nipkow
*** empty log message ***
1998-11-12, by nipkow
mesontest2.ML was never needed in the distribution
1998-11-12, by paulson
changed inverse syntax from x-| to i(x)
1998-11-12, by paulson
proved surjI
1998-11-11, by paulson
tidied
1998-11-11, by paulson
Big simplification of proofs.
1998-11-11, by paulson
tiny changes;
1998-11-10, by mueller
changed to a link;
1998-11-10, by mueller
local simpset theory data;
1998-11-09, by wenzelm
local claset theory data;
1998-11-09, by wenzelm
Object logic specific operations.
1998-11-09, by wenzelm
Isar setups;
1998-11-09, by wenzelm
added metacuts_tac;
1998-11-09, by wenzelm
removed local_theory;
1998-11-09, by wenzelm
exnMessage Interrupt;
1998-11-09, by wenzelm
added lift_modifier, rule;
1998-11-09, by wenzelm
added Isar;
1998-11-09, by wenzelm
added Isar/;
1998-11-09, by wenzelm
Pure outer syntax.
1998-11-09, by wenzelm
Non-logical toplevel commands.
1998-11-09, by wenzelm
Derived theory operations.
1998-11-09, by wenzelm
The global Isabelle/Isar outer syntax.
1998-11-09, by wenzelm
The Isabelle/Isar toplevel.
1998-11-09, by wenzelm
Histories of proof states, with undo / redo and prev / back.
1998-11-09, by wenzelm
Generic parsers for Isabelle/Isar outer syntax.
1998-11-09, by wenzelm
Outer lexical syntax for Isabelle/Isar.
1998-11-09, by wenzelm
Proof methods.
1998-11-09, by wenzelm
Symbolic theorem attributes.
1998-11-09, by wenzelm
Concrete argument syntax (for attributes, methods etc.).
1998-11-09, by wenzelm
Type-safe interface for proof context data.
1998-11-09, by wenzelm
Proof states and methods.
1998-11-09, by wenzelm
Proof context information.
1998-11-09, by wenzelm
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
1998-11-09, by wenzelm
Check release name and date in NEWS!
1998-11-09, by wenzelm
smart interrupt handler;
1998-11-09, by wenzelm
option -I: startup Isar interaction mode;
1998-11-09, by wenzelm
isabelle -I;
1998-11-09, by wenzelm
fake interrupt handler;
1998-11-09, by wenzelm
simple interrupt_handler;
1998-11-09, by wenzelm
new Domain/Range rules
1998-11-09, by paulson
new TIMES/Sigma rules
1998-11-09, by paulson
removed obsolete comment and "open" declaration
1998-11-09, by paulson
"Subscribe" link
1998-11-06, by paulson
spell check;
1998-11-06, by wenzelm
tuned;
1998-11-06, by wenzelm
added mailing list, removed mirrors;
1998-11-06, by mueller
Revising the Client proof as suggested by Michel Charpentier. New lemmas
1998-11-06, by paulson
made more generic;
1998-11-05, by mueller
Shortened names and added new thm.
1998-11-05, by nipkow
Some streamlining of text.
1998-11-04, by paulson
tuned;
1998-11-03, by wenzelm
tuned width of pics;
1998-11-03, by wenzelm
tuned;
1998-11-03, by wenzelm
oops;
1998-11-02, by wenzelm
tuned pics;
1998-11-02, by wenzelm
made weblint happy;
1998-11-02, by wenzelm
oops;
1998-11-02, by wenzelm
Id;
1998-11-02, by wenzelm
tuned;
1998-11-02, by wenzelm
tuned;
1998-11-02, by wenzelm
main Isabelle page;
1998-11-02, by wenzelm
New example
1998-11-02, by nipkow
Domain r, Range r replace fst``r, snd``r
1998-11-02, by paulson
increased precedence of unary minus from 80 to 100
1998-11-02, by paulson
increased precedence of unary minus from 80 to 100
1998-11-02, by paulson
Charpentier laws
1998-10-31, by paulson
the Increasing operator
1998-10-31, by paulson
no need for int_0
1998-10-31, by paulson
locales now implicitly quantify over free variables
1998-10-31, by paulson
tuned current_goals_markers;
1998-10-30, by wenzelm
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
1998-10-30, by paulson
Explicit (and improved) simprules for binary arithmetic.
1998-10-30, by paulson
*** empty log message ***
1998-10-29, by wenzelm
shyps note for prim. rules;
1998-10-29, by wenzelm
tuned;
1998-10-29, by wenzelm
tuned current_goals_markers semantics to avoid empty lines;
1998-10-29, by wenzelm
tidied
1998-10-29, by paulson
auto update
1998-10-29, by paulson
Some more proofs.
1998-10-28, by nipkow
added nat_diff_split and a few lemmas in Trancl.
1998-10-28, by nipkow
ML_SYSTEM=polyml-3.1;
1998-10-26, by wenzelm
tuned checklist;
Isabelle98-1
1998-10-25, by wenzelm
official release;
1998-10-24, by wenzelm
ML_SYSTEM factory default;
1998-10-24, by wenzelm
*** empty log message ***
1998-10-24, by wenzelm
tuned;
1998-10-24, by wenzelm
records;
1998-10-24, by wenzelm
*** empty log message ***
1998-10-24, by wenzelm
Added theorem bool_induct (for rep_datatype).
1998-10-23, by berghofe
Added theorem unit_induct (for rep_datatype).
1998-10-23, by berghofe
Added theorems True_not_False and False_not_True
1998-10-23, by berghofe
unit and bool are now represented as datatypes.
1998-10-23, by berghofe
corrected auto_tac (applications of unsafe wrappers)
1998-10-23, by oheimb
corrected (and simplified) depth_tac
1998-10-23, by oheimb
corrected auto_tac (applications of unsafe wrappers)
1998-10-23, by oheimb
corrected auto_tac (applications of unsafe wrappers)
1998-10-23, by oheimb
added SOLVE tactical
1998-10-23, by oheimb
tuned;
1998-10-23, by wenzelm
matharray;
1998-10-23, by wenzelm
SYNC: records (draft version);
1998-10-23, by wenzelm
Warns when stack is extended; better decl of print_depth
1998-10-23, by paulson
better checking of "defines" in a locale
1998-10-23, by paulson
better reporting of "Additional hypotheses" in a locale
1998-10-23, by paulson
Now users will never see (int 0)
1998-10-23, by paulson
auto update
1998-10-23, by paulson
updated as requested by Markus
1998-10-23, by paulson
export is_ml_identifier;
1998-10-23, by wenzelm
Updated to new datatype package.
1998-10-23, by berghofe
ex/Points added
1998-10-23, by narasche
Example for records
1998-10-23, by narasche
Directory Induct: Added new theory ABexp, removed obsolete
1998-10-23, by berghofe
Added new theory ABexp, removed obsolete theory Simult.
1998-10-23, by berghofe
Terms are now defined using the new datatype package.
1998-10-23, by berghofe
New example for using the datatype package:
1998-10-23, by berghofe
Removed obsolete theory Simult (see theory Term).
1998-10-23, by berghofe
started to add records;
1998-10-23, by wenzelm
occurs check now handles Bound variables (for soundness)
1998-10-23, by paulson
updated by isatool logo;
1998-10-23, by wenzelm
tuned block indent;
1998-10-22, by wenzelm
current_goals_markers;
1998-10-22, by wenzelm
some additions for Proof General by David Aspinall;
1998-10-22, by wenzelm
support current_goals_markers ref variable for print_current_goals;
1998-10-22, by wenzelm
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
1998-10-22, by wenzelm
fixed index.html;
1998-10-22, by wenzelm
tuned;
1998-10-22, by wenzelm
tuned;
1998-10-22, by wenzelm
standard Blast_tac demos
1998-10-22, by paulson
tidying
1998-10-22, by paulson
locales
1998-10-22, by paulson
Changed interface of inductive.
1998-10-21, by berghofe
Changed interface of rep_datatype: Characteristic theorems
1998-10-21, by berghofe
Changed interface.
1998-10-21, by berghofe
Changed interface of add_inductive: monos and con_defs are now
1998-10-21, by berghofe
Changed syntax of inductive.
1998-10-21, by berghofe
Changed syntax of rep_datatype and inductive: Theorems
1998-10-21, by berghofe
Added theorem prod_induct (needed for rep_datatype).
1998-10-21, by berghofe
Changed syntax of rep_datatype.
1998-10-21, by berghofe
fixed field_injects;
1998-10-21, by wenzelm
tuned;
1998-10-21, by wenzelm
no open;
1998-10-21, by wenzelm
tuned;
1998-10-21, by wenzelm
Tutorial
1998-10-21, by nipkow
dropped support for SML/NJ 109.x;
1998-10-21, by wenzelm
field_injects [iffs];
1998-10-21, by wenzelm
record_split_name;
1998-10-21, by wenzelm
tuned (all proofs are INSTABLE by David's definition of instability);
1998-10-21, by wenzelm
improved var names;
1998-10-21, by wenzelm
tuned stack_overflow_handler;
1998-10-20, by wenzelm
made SML/NJ happy;
1998-10-20, by wenzelm
delSWrapper "record_split_tac";
1998-10-20, by wenzelm
fixed Syntax module;
1998-10-20, by wenzelm
split_paired_all.ML;
1998-10-20, by wenzelm
field types: datatype;
1998-10-20, by wenzelm
quiet_mode, message;
1998-10-20, by wenzelm
quiet proofs;
1998-10-20, by wenzelm
fixed Syntax module;
1998-10-20, by wenzelm
Datatype instead of Prod;
1998-10-20, by wenzelm
QUIET_BREADTH_FIRST;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
simple Env replaced by Symtab;
1998-10-20, by wenzelm
added unvarify(T);
1998-10-20, by wenzelm
Syntax.max_pri;
1998-10-20, by wenzelm
Symtab.foldl;
1998-10-20, by wenzelm
quiet_mode, message;
1998-10-20, by wenzelm
structure Hidden = struct end;
1998-10-20, by wenzelm
hiding private stuff;
1998-10-20, by wenzelm
Symtab.foldl;
1998-10-20, by wenzelm
added foldl, keys;
1998-10-20, by wenzelm
split_paired_all.ML: turn surjective pairing into split rule;
1998-10-20, by wenzelm
updated
1998-10-20, by paulson
updated the MLWorks description
1998-10-20, by paulson
another little bug ;-) and minor changes in TLS.*;
1998-10-19, by mueller
little bug ;-)
1998-10-19, by mueller
added keyword 'and'
1998-10-19, by oheimb
corrected Header
1998-10-19, by oheimb
Addsimps [max_le_iff_conj];
1998-10-19, by nipkow
changed Super_L and Hyper_R to left and right Meta
1998-10-19, by oheimb
layout
1998-10-19, by oheimb
solved conflict by taking newest version;
1998-10-19, by mueller
added Clarify_tac to speed up proofs
1998-10-19, by paulson
moved a theorem
1998-10-19, by paulson
fixed comment
1998-10-19, by paulson
fixed some indenting; changed a VERY slow blast_tac to fast_tac
1998-10-19, by paulson
updated, tuned;
1998-10-18, by wenzelm
added Minho (Portugal);
1998-10-18, by wenzelm
Fixed bug (improper handling of flag flat_names).
1998-10-16, by berghofe
Added quiet_mode flag.
1998-10-16, by berghofe
- Changed structure of name spaces
1998-10-16, by berghofe
tuned MLWorks options;
1998-10-16, by wenzelm
MLWorks 2.0;
1998-10-16, by wenzelm
Changed structure of name spaces for datatypes.
1998-10-16, by berghofe
2. The simplifier now knows a little bit about nat-arithmetic.
1998-10-16, by nipkow
Mods because trans_tac is now part of thge simplifier.
1998-10-16, by nipkow
Mods because of: Installed trans_tac in solver of simpset().
1998-10-16, by nipkow
Installed trans_tac in solver of simpset().
1998-10-16, by nipkow
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
1998-10-16, by paulson
parent is Main
1998-10-16, by paulson
*** empty log message ***
1998-10-16, by nipkow
integer simprocs
1998-10-15, by paulson
Uses overload_1st_set to specify overloading
1998-10-15, by paulson
specifications as sets of programs
1998-10-15, by paulson
Description of new version.
1998-10-14, by nipkow
New many-sorted version.
1998-10-14, by nipkow
See (* FIXME zero_neq_conv *)
1998-10-14, by nipkow
Nat: added zero_neq_conv
1998-10-14, by nipkow
added Int.int;
1998-10-13, by wenzelm
PRIVATE sig parts;
1998-10-13, by wenzelm
length_Suc_conv is no longer given to AddIffs
1998-10-13, by paulson
new theorems
1998-10-13, by paulson
tidied
1998-10-13, by paulson
Addition of HOL/UNITY/Client
1998-10-13, by paulson
new rule
1998-10-13, by paulson
Addition of HOL/UNITY/Client
1998-10-13, by paulson
Unified treatment of type error msgs.
1998-10-09, by nipkow
More pretty breaks in error msgs.
1998-10-09, by nipkow
Added a few breaks in error text.
1998-10-09, by nipkow
new theorem
1998-10-09, by paulson
new theorems
1998-10-09, by paulson
new guarantees laws
1998-10-09, by paulson
renamed Suc_card_Diff or something
1998-10-09, by nipkow
Multisets at last!
1998-10-09, by nipkow
added Induct/Multiset*
1998-10-09, by nipkow
New inductive definition of `card'
1998-10-09, by nipkow
polymorphic versions of nat_neq_iff and nat_neqE
1998-10-09, by paulson
Further improvement of the simplifier.
1998-10-08, by nipkow
Tuned simplifier not to re-normalized already normalized terms.
1998-10-07, by nipkow
tuned rm CVS;
1998-10-07, by wenzelm
runs test
1998-10-07, by nipkow
tidying and renaming
1998-10-07, by paulson
new theorems
1998-10-07, by paulson
tidied
1998-10-07, by paulson
new files UNITY/Comp.{thy,ML}
1998-10-07, by paulson
Merges FoldSet into Finite
1998-10-06, by nipkow
deleted incorrect code that set Goals.proof_timing:=false
1998-10-05, by paulson
Now prove_goalw_cterm never prints timing statistics
1998-10-05, by paulson
MLWorks demands the "op" before $
1998-10-05, by paulson
Finished proofs to end of section 5.1 of Chandy and Sanders
1998-10-05, by paulson
Join now an infix operator
1998-10-05, by paulson
simpler interface for Abel_Cancel
1998-10-05, by paulson
tidied
1998-10-05, by paulson
id <-> Id
1998-10-02, by nipkow
added Real to BasisLibrary
1998-10-02, by paulson
new file Provers/Arith/abel_cancel.ML
1998-10-02, by paulson
new files Provers/Arith/abel_cancel.ML and Real/simproc.ML
1998-10-02, by paulson
tidying
1998-10-02, by paulson
white border -- disabled;
1998-10-01, by wenzelm
Improved definition of foldSet.
1998-10-01, by nipkow
revised for new treatment of integers
1998-10-01, by paulson
new singleton_conv2
1998-10-01, by nipkow
tidied
1998-10-01, by paulson
a few new lemmas.
1998-10-01, by nipkow
composition theory
1998-10-01, by paulson
abstype of programs
1998-10-01, by paulson
now invokes functor
1998-10-01, by paulson
much tidying
1998-10-01, by paulson
new lemmas
1998-10-01, by paulson
better handling of literals
1998-10-01, by paulson
tidied
1998-10-01, by paulson
white space
1998-10-01, by paulson
new simproc functor
1998-10-01, by paulson
Revised version with Abelian group simprocs
1998-10-01, by paulson
handle empty name;
1998-09-29, by wenzelm
auto update
1998-09-29, by paulson
new function inter_term
1998-09-29, by paulson
Now id:(Acts prg) is implicit
1998-09-29, by paulson
modified proof for new simproc
1998-09-29, by paulson
many renamings and changes. Simproc for cancelling common terms in relations
1998-09-29, by paulson
New keywords
1998-09-29, by nipkow
Revised wf_acc_iff and Co.
1998-09-29, by nipkow
new: wfUNIVI
1998-09-29, by nipkow
Package now chooses type variable names more carefully to
1998-09-26, by berghofe
minor corrections
1998-09-25, by oheimb
exchanged automatic-tactics and semi-automatic-tactics
1998-09-25, by oheimb
improved indentation
1998-09-25, by oheimb
rearranged SIMPSET(');
1998-09-25, by wenzelm
*** empty log message ***
1998-09-25, by wenzelm
isatool logo;
1998-09-25, by wenzelm
added isatool logo;
1998-09-25, by wenzelm
improved;
1998-09-25, by wenzelm
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
added Int to BasisLibrary
1998-09-25, by paulson
deleted illegal "op"
1998-09-25, by paulson
uses BasisLibrary for Int.min
1998-09-25, by paulson
patched obsolete code
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*
1998-09-25, by paulson
Now uses integers instead of naturals
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
tuned;
1998-09-25, by wenzelm
tuned pretty_tag;
1998-09-25, by wenzelm
added REPEAT1;
1998-09-25, by wenzelm
create an instance of the Isabelle logo;
1998-09-24, by wenzelm
generic eps version;
1998-09-24, by wenzelm
simplified CLASIMP_DATA
1998-09-24, by oheimb
removed addcongs2 and delcongs2
1998-09-24, by oheimb
renamed mk_meta_eq to mk_eq
1998-09-24, by oheimb
simplified CLASIMP_DATA
1998-09-24, by oheimb
renamed some axioms; some new theorems
1998-09-24, by paulson
introduced addSE2, addSD2, addE2, and addD2
1998-09-24, by oheimb
improved description of looper and splitter
1998-09-24, by oheimb
workaround for litte bug in our ln command
1998-09-24, by oheimb
Function nat_of now maps negative integers to zero, not their absolute value
1998-09-24, by paulson
renamed some axioms
1998-09-24, by paulson
added correctness proofs for arithmetic
1998-09-24, by paulson
new induction rule for integers
1998-09-24, by paulson
fixed calls of ln, rm
1998-09-24, by oheimb
changed xnum token syntax;
1998-09-23, by wenzelm
unary minus
1998-09-23, by paulson
much renaming and reorganization
1998-09-23, by paulson
New directory Integ for the integers
1998-09-23, by paulson
a few new theorems
1998-09-23, by paulson
deleted needless parentheses
1998-09-23, by paulson
tidying and deleting needless parentheses
1998-09-23, by paulson
deleted needless parentheses
1998-09-23, by paulson
tuned Isamode;
1998-09-22, by wenzelm
re-organized for the new directory Integ
1998-09-22, by paulson
new directory for Integers
1998-09-22, by paulson
deleted erroneous semicolon
1998-09-22, by paulson
tidying
1998-09-22, by paulson
tidying
1998-09-22, by paulson
new directory for Integers
1998-09-22, by paulson
big tidying of simpsets, etc
1998-09-22, by paulson
*** empty log message ***
1998-09-21, by oheimb
improved addbefore and addSbefore
1998-09-21, by oheimb
*** empty log message ***
1998-09-21, by oheimb
added addD2, addE2, addSD2, and addSE2
1998-09-21, by oheimb
improved indentation
1998-09-21, by oheimb
added wrapper for bspec
1998-09-21, by oheimb
added addD2, addE2, addSD2, and addSE2
1998-09-21, by oheimb
re-added mem and list_all
1998-09-21, by oheimb
re-added mem and list_all
1998-09-21, by oheimb
added dependance on HOL
1998-09-21, by oheimb
added indentation
1998-09-21, by oheimb
simplified proof
1998-09-21, by oheimb
inserted space in #-1 to prevent confusion with an integer constant
1998-09-21, by paulson
Unary minus is now #- and not #~
1998-09-21, by paulson
much renaming and tidying
1998-09-21, by paulson
leaves subgoal package empty
1998-09-18, by paulson
improved (but still flawed) treatment of binary arithmetic
1998-09-18, by paulson
Now defines "int" as a linear order; basic derivations moved to IntDef
1998-09-18, by paulson
new files in Integ
1998-09-18, by paulson
simpler definition of zmagnitude, and new thms for it
1998-09-18, by paulson
stronger version of theI2
1998-09-18, by paulson
tidied
1998-09-18, by paulson
new theorem less_imp_Suc_add
1998-09-18, by paulson
new files in Integ
1998-09-18, by paulson
new theorem less_Suc_eq_le
1998-09-18, by paulson
new files in Integ
1998-09-18, by paulson
new theorem less_Suc_eq_le and le_simps
1998-09-18, by paulson
updated comments
1998-09-18, by paulson
tidying
1998-09-18, by paulson
theorem le_diff_conv2; tidying and expandshort
1998-09-18, by paulson
Pruning of parameters and True assumptions
1998-09-18, by paulson
Suppress timing messages for theorems proved in theory sections
1998-09-18, by paulson
improved error messages
1998-09-18, by paulson
deleted redundant quantifiers
1998-09-16, by paulson
From Compl(A) to -A
1998-09-15, by paulson
revised treatment of integers
1998-09-15, by paulson
From Compl(A) to -A
1998-09-15, by paulson
Function 'step' is already defined in NA.thy.
1998-09-15, by nipkow
tidied
1998-09-15, by paulson
commented out duplicate proof
1998-09-14, by paulson
simpler proof
1998-09-14, by paulson
new theorem le_diff_conv
1998-09-14, by paulson
Extra steps at end to make it run faster
1998-09-11, by paulson
added clarsimp_tac and Clarsimp_tac
1998-09-11, by oheimb
tidied using locales
1998-09-11, by paulson
Less deterministic reconstruction: now more robust but perhaps slower
1998-09-11, by paulson
tidied
1998-09-11, by paulson
fixed PROOF FAILED
1998-09-11, by paulson
fixed comment
1998-09-11, by paulson
stabilized proof of card_mono
1998-09-11, by oheimb
corrected indentation
1998-09-11, by oheimb
equals0D
1998-09-10, by paulson
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
1998-09-10, by paulson
added proof of final result...
1998-09-10, by paulson
tidied
1998-09-10, by paulson
Now WO1_WO7 has a .thy file
1998-09-10, by paulson
eliminated equals0E
1998-09-10, by paulson
fixed PROOF FAILED
1998-09-10, by paulson
tidied
1998-09-10, by paulson
deleted the bogus equals0E, fixed equals0D
1998-09-10, by paulson
eliminated equals0E
1998-09-10, by paulson
well-formed asym rules
1998-09-10, by paulson
new file AC/WO1_WO7.thy
1998-09-10, by paulson
Allows more backtracking in proof reconstruction, making it slower but more
1998-09-10, by paulson
a step to help a proof
1998-09-10, by paulson
new entries
1998-09-10, by paulson
deleted not_Says_to_self
1998-09-10, by paulson
well-formed asym rules; misc. tidying
1998-09-10, by paulson
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
1998-09-10, by paulson
tidied, fixing PROOF FAILED
1998-09-10, by paulson
tidied
1998-09-10, by paulson
tidied, eliminating hard proof
1998-09-10, by paulson
well-formed zless_asym; tidied
1998-09-10, by paulson
patch to stop failing proof
1998-09-10, by paulson
New theorem wf_not_sym and well-formed wf_asym
1998-09-10, by paulson
tided the unused rule irrefl_tranclI
1998-09-10, by paulson
Changed equals0E back to equals0D and gave it the correct destruct form
1998-09-10, by paulson
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
1998-09-10, by paulson
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
1998-09-10, by paulson
Proved and added rewrite rule (@x. x=y) = y to simpset.
1998-09-09, by nipkow
reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
1998-09-09, by oheimb
AddIffs[not_None_eq];
1998-09-09, by oheimb
AddSDs[override_SomeD];
1998-09-09, by oheimb
changed constants mem and list_all to mere translations
1998-09-09, by oheimb
changed order of included theories
1998-09-09, by oheimb
added Id_apply
1998-09-09, by oheimb
removed superfluous AddIs thms (were already in)
1998-09-09, by oheimb
renamed sswhen to sscase
1998-09-09, by oheimb
simplified definition of axclass cpo
1998-09-09, by oheimb
added caveat; a real solution would be difficult
1998-09-08, by oheimb
improved spacing
1998-09-08, by oheimb
adapted modifiers: Mod1 -> Mod2, Mod5 -> Mod4
1998-09-08, by oheimb
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
1998-09-08, by paulson
Got rid of not_Says_to_self; re-organized proofs
1998-09-08, by paulson
new example; tidying
1998-09-07, by paulson
new example
1998-09-07, by paulson
New UNITY theory, the N-S protocol
1998-09-07, by paulson
tidying
1998-09-07, by paulson
Function 'upt'
1998-09-04, by nipkow
Arith: less_diff_conv
1998-09-04, by nipkow
A new approach, using simp_of_act and simp_of_set to activate definitions when
1998-09-03, by paulson
Added function upto to List.
1998-09-02, by nipkow
modified proofs for new constrains_tac and ensures_tac
1998-09-02, by paulson
two new thms
1998-09-02, by paulson
Moved constrains_tac from SubstAx to Constrains.
1998-09-02, by paulson
small simplification to not_Says_to_self
1998-09-02, by paulson
New approach, using a locale
1998-09-01, by paulson
tidied
1998-09-01, by paulson
Replaced Suc_diff_n by Suc_diff_le
1998-09-01, by paulson
new theory Induct/FoldSet
1998-09-01, by paulson
New law card_Un_Int. Removed card_insert from simpset
1998-09-01, by paulson
tidying; moved diff_less to Arith.ML
1998-09-01, by paulson
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
1998-09-01, by paulson
New lemmas involving Int
1998-09-01, by paulson
New lemmas involving Int
1998-09-01, by paulson
fixed error msg
1998-09-01, by paulson
Moved lemmas to Arith.ML
1998-09-01, by paulson
Two new subtraction lemmas
1998-09-01, by paulson
made SML/NJ happy;
1998-08-30, by wenzelm
* print mode 'emacs' reserved for Isamode;
1998-08-28, by wenzelm
added emacs mode;
1998-08-28, by wenzelm
tuned isatool install;
1998-08-28, by wenzelm
tuned;
1998-08-28, by wenzelm
-d DISTDIR;
1998-08-28, by wenzelm
tuned;
1998-08-28, by wenzelm
www.in.tum.de;
1998-08-27, by wenzelm
made tutorial first;
1998-08-27, by wenzelm
tuned;
1998-08-27, by wenzelm
exec;
1998-08-27, by wenzelm
* Pure: ML function 'theory_of' replaced by 'theory';
1998-08-27, by wenzelm
tuned;
1998-08-27, by wenzelm
isatool install;
1998-08-27, by wenzelm
added tutorial;
1998-08-27, by wenzelm
fixed ISABELLE_USEDIR_OPTIONS;
1998-08-27, by wenzelm
*** empty log message ***
1998-08-27, by wenzelm
Goal, Goalw;
1998-08-27, by wenzelm
moeved get_thm etc. to goals.tex;
1998-08-27, by wenzelm
tuned doc name;
1998-08-27, by wenzelm
fixed center;
1998-08-27, by wenzelm
ISABELLE_USEDIR_OPTIONS="-i false";
1998-08-27, by wenzelm
tuned;
1998-08-27, by wenzelm
eps logis;
1998-08-27, by wenzelm
href eps versions;
1998-08-27, by wenzelm
weblinted, tuned;
1998-08-27, by wenzelm
fake proper eps header;
1998-08-27, by wenzelm
fixed tutorial;
1998-08-26, by wenzelm
added HOL tutorial;
1998-08-26, by wenzelm
added HOL tutorial;
1998-08-26, by wenzelm
junk
1998-08-26, by nipkow
*** empty log message ***
1998-08-26, by nipkow
*** empty log message ***
1998-08-26, by nipkow
The HOL tutorial.
1998-08-26, by nipkow
moved images to gfx dir;
1998-08-26, by wenzelm
tuned;
1998-08-24, by wenzelm
SYNC;
1998-08-24, by wenzelm
emacs local vars;
1998-08-24, by wenzelm
emacs local vars;
1998-08-24, by wenzelm
added nonterminals, setup;
1998-08-24, by wenzelm
added Antiquote example;
1998-08-24, by wenzelm
mkdir -p;
1998-08-24, by wenzelm
emacs local vars;
1998-08-24, by wenzelm
SYNC;
1998-08-24, by wenzelm
emacs local vars;
1998-08-24, by wenzelm
isatool install;
1998-08-24, by wenzelm
install binaries with absolute references to ISABELLE_HOME/bin;
1998-08-24, by wenzelm
debugged split_eta_proc
1998-08-24, by oheimb
tidied
1998-08-21, by paulson
Tidying
1998-08-21, by paulson
New UNITY files
1998-08-21, by paulson
New theory Lift
1998-08-20, by paulson
new theorems
1998-08-20, by paulson
tidied
1998-08-20, by paulson
new theorems; adds [le_refl, less_imp_le] as simprules
1998-08-20, by paulson
adjusted for new rewrites
1998-08-20, by paulson
tidied
1998-08-20, by paulson
tidied
1998-08-20, by paulson
Must remove leD from simpset
1998-08-20, by paulson
tidied
1998-08-20, by paulson
Must remove less_imp_le from simpset
1998-08-20, by paulson
Added converse_rtranclE(2)
1998-08-20, by nipkow
Now qed_spec_mp respects locales, by calling ml_store_thm
1998-08-20, by paulson
fixed param;
1998-08-19, by wenzelm
assume: adjust_maxidx;
1998-08-19, by wenzelm
new version, more resistant to PROOF FAILED. Now it distinguishes between
1998-08-19, by paulson
The warning "Rewrite rule from different theory" is ALWAYS printed, even if
1998-08-19, by paulson
new theorem zero_less_diff
1998-08-19, by paulson
Misc changes
1998-08-19, by paulson
Deleted obsolete declaration of PartE'
1998-08-19, by paulson
Tidied, removing uses of less_imp_diff_positive
1998-08-19, by paulson
tidied
1998-08-19, by paulson
fixed overloading of "image"
1998-08-19, by paulson
Overloading decl should assist Blast_tac
1998-08-19, by paulson
less_imp_diff_positive is redundant with new simprule zero_less_diff
1998-08-19, by paulson
Some new theorems. zero_less_diff replaces less_imp_diff_positive
1998-08-19, by paulson
ZF.thy
1998-08-18, by paulson
new theorem Un_Diff_Int
1998-08-18, by paulson
added comment
1998-08-18, by paulson
new theorem diff_Suc_less_diff
1998-08-18, by paulson
added get_tthmss;
1998-08-17, by wenzelm
Mention RegExp2NA.
1998-08-17, by nipkow
expandshort
1998-08-17, by paulson
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
1998-08-17, by paulson
Now allows "." in rule names, with special treatment for "be"
1998-08-17, by paulson
Direct translation RegExp -> NA!
1998-08-17, by nipkow
Additions to Lex.
1998-08-17, by nipkow
got rid of some goal thy commands
1998-08-14, by paulson
now trans_tac is part of the claset...
1998-08-14, by paulson
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
1998-08-14, by paulson
expandshort
1998-08-14, by paulson
Uses Goal instead of "goal...thy" to avoid theory problems
1998-08-14, by paulson
even more tidying of Goal commands
1998-08-13, by paulson
tidying
1998-08-13, by paulson
Moved the definition of s_u (as s) into the locale
1998-08-13, by paulson
Constrains, Stable, Invariant...more of the substitution axiom, but Union
1998-08-13, by paulson
simpler SELECT_GOAL no longer inserts a dummy parameter
1998-08-13, by paulson
Rule mk_triv_goal for making instances of triv_goal
1998-08-13, by paulson
Blast_tac is faster
1998-08-13, by paulson
stac now handles definitions as well as equalities
1998-08-13, by paulson
stac
1998-08-13, by paulson
minor adaption for SML/NJ
1998-08-12, by oheimb
added theorems Id_o, o_Id
1998-08-12, by oheimb
cleanup for Fun.thy:
1998-08-12, by oheimb
the splitter is now defined as a functor
1998-08-12, by oheimb
renamed mk_meta_eq to meta_eq
1998-08-12, by oheimb
removed superfluous o_apply
1998-08-12, by oheimb
streamlined proofs with new hoare_conseq1, hoare_conseq2
1998-08-12, by oheimb
defined map_upd by translation via fun_upd
1998-08-12, by oheimb
added Eps_eq
1998-08-12, by oheimb
removed use_thys implied by use_thy "Main"
1998-08-12, by oheimb
repaired proof of chfindom_monofun2cont
1998-08-12, by oheimb
added length_Suc_conv, finite_set
1998-08-12, by oheimb
replaced idt by pttrn in @filter
1998-08-12, by oheimb
replaced split_etas by split_eta_proc
1998-08-12, by oheimb
added ospec
1998-08-12, by oheimb
minor correction: n must not be used as free variable
1998-08-12, by oheimb
eliminated fabs,fapp.
1998-08-12, by slotosch
suffix, unsuffix moved to Pure/library.ML;
1998-08-10, by wenzelm
fixed comment;
1998-08-10, by wenzelm
tuned;
1998-08-10, by wenzelm
??id syntax for text variables;
1998-08-10, by wenzelm
dest_binding, dest_skolem;
1998-08-10, by wenzelm
val single: 'a -> 'a list;
1998-08-10, by wenzelm
Tidying of AC, especially of AC16_WO4 using a locale
1998-08-10, by paulson
More lemmas about lex.
1998-08-10, by nipkow
*** empty log message ***
1998-08-08, by nipkow
List now contains some lexicographic orderings.
1998-08-08, by nipkow
added store_tthm;
1998-08-06, by wenzelm
Improved well-formedness check.
1998-08-06, by berghofe
even more tidying of Goal commands
1998-08-06, by paulson
A higher-level treatment of LeadsTo, minimizing use of "reachable"
1998-08-06, by paulson
Simplified proof!!
1998-08-06, by nipkow
*** empty log message ***
1998-08-06, by nipkow
Lemma renamed in HOL.
1998-08-06, by nipkow
Added macro `termi'
1998-08-06, by nipkow
New lemmas in List and Lambda in IsaMakefile
1998-08-06, by nipkow
Removed duplicate thms (see comment to Arith.ML)
1998-08-06, by nipkow
Removed duplicate thms:
1998-08-06, by nipkow
Removed comments.
1998-08-06, by nipkow
even more tidying of Goal commands
1998-08-06, by paulson
disjointness
1998-08-06, by paulson
Now recognizes both {}= and ={}
1998-08-06, by paulson
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
1998-08-06, by paulson
New result from AC directory
1998-08-06, by paulson
added solve_tac;
1998-08-06, by wenzelm
New results from AC
1998-08-06, by paulson
First steps towards termination of simply typed terms.
1998-08-06, by nipkow
binding / skolem vars;
1998-08-06, by wenzelm
Null program and a few new results
1998-08-05, by paulson
Finished the example
1998-08-05, by paulson
Indentation, comments
1998-08-05, by paulson
Renamed equals0D to equals0E
1998-08-05, by paulson
Tidied
1998-08-05, by paulson
Removal of "disjoint" translation
1998-08-05, by paulson
New record type of programs
1998-08-05, by paulson
Union primitives and examples
1998-08-05, by paulson
tuned;
1998-08-04, by wenzelm
added LocaleGroup, PiSets examples;
1998-08-04, by wenzelm
added Open_locale, Close_locale;
1998-08-04, by wenzelm
added 'locale' section;
1998-08-04, by wenzelm
Locale.setup;
1998-08-04, by wenzelm
added export: thm -> thm;
1998-08-04, by wenzelm
moved print_goals to locale.ML;
1998-08-04, by wenzelm
added locale.ML;
1998-08-04, by wenzelm
added icons;
1998-08-04, by wenzelm
Renamed equals0D to equals0E
1998-08-04, by paulson
Renamed equals0D to equals0E; tidied
1998-08-04, by paulson
Constant "invariant" and new constrains_tac, ensures_tac
1998-08-04, by paulson
Tidying
1998-08-04, by paulson
Boolean quantification
1998-08-04, by paulson
Deleted the redundant rule mem_if
1998-08-04, by paulson
fixed disjount translation;
1998-08-04, by wenzelm
tuned comments;
1998-08-04, by wenzelm
Better comments
1998-08-03, by paulson
New rewrite rules for quantification over bounded UNIONs
1998-08-03, by paulson
Tidied; uses records
1998-07-31, by paulson
new theorems for partial funcs
1998-07-31, by paulson
Pretty.sym;
1998-07-31, by wenzelm
size / length: printable length;
1998-07-31, by wenzelm
isatool expandshort;
1998-07-31, by wenzelm
Removal of obsolete "open" commands from heads of .ML files
1998-07-31, by paulson
Replaced nat.exhaustion by nat.exhaust
1998-07-31, by berghofe
Removed HOL/IMP/Com.ML because it contained only an "open" declaration
1998-07-31, by paulson
tidied
1998-07-31, by paulson
Removal of obsolete "open" commands from heads of .ML files
1998-07-31, by paulson
Fixed primrec.
1998-07-30, by berghofe
Fixed primrec.
1998-07-30, by berghofe
made SML/NJ happy;
1998-07-30, by wenzelm
functorized Clasimp module;
1998-07-30, by wenzelm
fixed primrec;
1998-07-30, by wenzelm
tuned;
1998-07-30, by wenzelm
Equations are now stored in theory.
1998-07-30, by berghofe
Deleted obsolete comments.
1998-07-30, by berghofe
Adapted to new datatype package.
1998-07-30, by berghofe
Script that adapts theories and proof scripts to new datatype package.
1998-07-30, by berghofe
make_defs not marked as internal;
1998-07-30, by wenzelm
late setup of Pure and CPure;
1998-07-29, by wenzelm
removed global_names flag;
1998-07-28, by wenzelm
theory_of renamed to theory (and made public);
1998-07-28, by wenzelm
added Real structure (taken from SML/NJ basis lib);
1998-07-28, by wenzelm
tuned;
1998-07-28, by wenzelm
Tidied
1998-07-28, by paulson
Changed "goal" to "Goal"
1998-07-28, by paulson
Updated examples
1998-07-28, by paulson
A little quantifier duplication for IFOL
1998-07-27, by paulson
A few new lemmas by Mark Staples
1998-07-27, by paulson
tuned;
1998-07-27, by wenzelm
conversion bug in simpproc list_eq
1998-07-27, by nipkow
added ex/MonoidGroups (record example);
1998-07-24, by wenzelm
added type and update syntax;
1998-07-24, by wenzelm
added more_update;
1998-07-24, by wenzelm
update -> fun_upd
1998-07-24, by nipkow
Map.update -> map_upd, Unpdate.update -> fun_upd
1998-07-24, by nipkow
added internal;
1998-07-24, by wenzelm
Adapted to new datatype package.
1998-07-24, by berghofe
Adapted to new datatype package.
1998-07-24, by berghofe
Renamed '$' to 'Scons' because of clashes with constants of the same
1998-07-24, by berghofe
Added functions addIffs and delIffs which operate on clasimpsets.
1998-07-24, by berghofe
Added theorem distinct_lemma (needed for datatypes).
1998-07-24, by berghofe
Declaration of type 'nat' as a datatype (this allows usage of
1998-07-24, by berghofe
Removed nat_case, nat_rec, and natE (now provided by datatype
1998-07-24, by berghofe
Removed ThyData setup.
1998-07-24, by berghofe
Added theorem ex1_implies_ex.
1998-07-24, by berghofe
Adapted to new datatype package.
1998-07-24, by berghofe
Adapted to new datatype package.
1998-07-24, by berghofe
Removed old datatype package.
1998-07-24, by berghofe
New theory Datatype. Needed as an ancestor when defining datatypes.
1998-07-24, by berghofe
Added new function add_typedef_i_no_def which doesn't add
1998-07-24, by berghofe
Replaced Nat.thy by NatDef.thy because Nat.thy depends on
1998-07-24, by berghofe
New primrec function definition package
1998-07-24, by berghofe
New datatype definition package
1998-07-24, by berghofe
induct_tac -> exhaust_tac in 2 places.
1998-07-24, by nipkow
moved long_names / cond_extern to name_space.ML;
1998-07-22, by wenzelm
tuned;
1998-07-22, by wenzelm
tuned;
1998-07-21, by wenzelm
fixed eps/ps find;
1998-07-21, by wenzelm
fixed CVSROOT;
1998-07-21, by wenzelm
fixed isabelle logo;
1998-07-21, by wenzelm
library includes Isabelle version information;
1998-07-21, by wenzelm
isatool expandshort;
1998-07-21, by wenzelm
fixed isabelle logo;
1998-07-21, by wenzelm
SYNC;
1998-07-21, by wenzelm
added pdfsetup and isabelle logo;
1998-07-20, by wenzelm
SYNC;
1998-07-20, by wenzelm
Added acc_downwards
1998-07-20, by nipkow
Added simproc list_eq.
1998-07-20, by nipkow
Simplified last proof.
1998-07-18, by nipkow
ZF: Main, Update
1998-07-17, by paulson
added case_tac to be like HOL
1998-07-17, by paulson
added Main and Update
1998-07-17, by paulson
as in HOL
1998-07-17, by paulson
A stronger apply_0, and new thm domain_lam
1998-07-17, by paulson
added comments
1998-07-17, by paulson
tidying
1998-07-17, by paulson
now with Goal cmd
1998-07-17, by paulson
tidying
1998-07-16, by paulson
Got rid of obsolete "goal" commands.
1998-07-16, by paulson
Addition of "Theorem B" of Peter Andrews
1998-07-16, by paulson
Fixed bug in transform_rule.
1998-07-15, by berghofe
More tidying and removal of "\!\!... from Goal commands
1998-07-15, by paulson
More tidying and removal of "\!\!... from Goal commands
1998-07-15, by paulson
@ -> $
1998-07-15, by nipkow
disjoint
1998-07-15, by nipkow
Minor tidying up.
1998-07-15, by nipkow
Removal of leading "\!\!..." from most Goal commands
1998-07-15, by paulson
new stac
1998-07-14, by paulson
CHANGED_GOAL added to declare a more robust stac
1998-07-14, by paulson
inj_on
1998-07-14, by nipkow
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
1998-07-14, by paulson
Corrected dead link.
1998-07-13, by nipkow
Huge tidy-up: removal of leading \!\!
1998-07-13, by paulson
massive tidying of proofs
1998-07-13, by paulson
renamed mutex to Acts
1998-07-13, by paulson
Replace awkward primrec by recdef.
1998-07-13, by nipkow
swapped condition in update_apply.
1998-07-13, by nipkow
isatool expandshort;
1998-07-12, by wenzelm
the distribution now includes Isabelle icons: see
1998-07-10, by wenzelm
added xpm icons;
1998-07-10, by wenzelm
Converted to Auto_tac
1998-07-06, by nipkow
several new basic modules made available for general use;
1998-07-03, by wenzelm
cleaned up;
1998-07-03, by wenzelm
theory Main includes everything;
1998-07-03, by wenzelm
reorganized the main HOL image;
1998-07-03, by wenzelm
stepping stones: Recdef, Main;
1998-07-03, by wenzelm
stepping stones;
1998-07-03, by wenzelm
removed duplicate thms;
1998-07-03, by wenzelm
moved String theory to main HOL;
1998-07-03, by wenzelm
Removed disjE from list of rules used to simplify elimination
1998-07-03, by berghofe
Removed leading !! in goals
1998-07-03, by nipkow
Removed leading !! in goals.
1998-07-03, by nipkow
Removed leading !! in goals.
1998-07-03, by nipkow
Renamed expand_if to split_if and setloop split_tac to addsplits,
1998-07-02, by paulson
HACKED declaration of addsplits
1998-07-02, by paulson
Deleted leading parameters thanks to new Goal command
1998-07-02, by paulson
tuned comment;
1998-07-02, by wenzelm
Symbol.beginning;
1998-07-02, by wenzelm
Uncurried functions LeadsTo and reach
1998-07-02, by paulson
fixed Integ;
1998-07-02, by wenzelm
Adapted to new inductive definition package.
1998-07-01, by berghofe
Fixed bug (improper handling of flag no_ind).
1998-07-01, by berghofe
Replaced "use_dir" command by "use", because nested calls
1998-07-01, by berghofe
HOL-Real
1998-07-01, by paulson
tuned Inductive.thy;
1998-07-01, by wenzelm
added add_typedecls;
1998-07-01, by wenzelm
Removed structure Prod_Syntax.
1998-06-30, by berghofe
Adapted to new inductive definition package.
1998-06-30, by berghofe
Adapted to new inductive package.
1998-06-30, by berghofe
Removed obsolete comments.
1998-06-30, by berghofe
Removed old inductive definition package.
1998-06-30, by berghofe
Removed structure Prod_Syntax.
1998-06-30, by berghofe
Adapted to new inductive definition package.
1998-06-30, by berghofe
Moved most of the Prod_Syntax - stuff to HOLogic.
1998-06-30, by berghofe
Added additional theorems needed for inductive definitions.
1998-06-30, by berghofe
New inductive definition package
1998-06-30, by berghofe
added quick_and_dirty flag;
1998-06-30, by wenzelm
moved actual (C)Pure theories to pure.ML;
1998-06-29, by wenzelm
tuned transaction;
1998-06-29, by wenzelm
use_text: verbose flag;
1998-06-29, by wenzelm
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
1998-06-26, by paulson
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
1998-06-26, by paulson
fixed unit_eq;
1998-06-25, by wenzelm
delsimprocs [unit_eq_proc];
1998-06-25, by wenzelm
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
1998-06-25, by wenzelm
tuned loose bound vars check;
1998-06-25, by wenzelm
added unit_eq simplification procedure;
1998-06-25, by wenzelm
added XX_YY_rewrite: simpset -> cterm -> thm;
1998-06-25, by wenzelm
Thm.rewrite_cterm;
1998-06-25, by wenzelm
defaults for free variables hide consts of same name;
1998-06-25, by wenzelm
added rewrite_cterm;
1998-06-25, by wenzelm
Installation of target HOL-Real
1998-06-25, by paulson
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
1998-06-24, by nipkow
Ran isatool fixgoal
1998-06-24, by paulson
removed duplicate entry for Goal
1998-06-24, by paulson
Trivial change to be more like paper
1998-06-24, by paulson
Tidying; renaming of Says_Server_message_form to
1998-06-24, by paulson
*** empty log message ***
1998-06-23, by nipkow
Consequences of the change from [ := ] to ( := ) in theory Update.
1998-06-23, by nipkow
Replaced [ := ] syntax by ( := ).
1998-06-23, by nipkow
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.
1998-06-22, by paulson
comments and minor tidying
1998-06-22, by paulson
simplified and tidied the proofs
1998-06-22, by paulson
check_mlhome_file;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
def_sort;
1998-06-20, by wenzelm
renamed Thm(s) back to thm(s);
1998-06-20, by wenzelm
export mk_triple1/2;
1998-06-20, by wenzelm
added read_def_axm;
1998-06-20, by wenzelm
added fix_mixfix;
1998-06-20, by wenzelm
fixed comment
1998-06-19, by paulson
tidying
1998-06-19, by paulson
New example Kerberos_BAN by G Bella
1998-06-19, by paulson
fixed comment;
1998-06-18, by wenzelm
tuned \s pattern;
1998-06-18, by wenzelm
isatool fixgoal;
1998-06-18, by wenzelm
removed Thy;
1998-06-18, by wenzelm
replaced warning by error_msg;
1998-06-18, by wenzelm
new toplevel commands `Goal' and `Goalw';
1998-06-18, by wenzelm
renamed thm(s) to Thm(s);
1998-06-18, by wenzelm
replace goal(w) commands by implicit versions Goal(w);
1998-06-18, by wenzelm
Goal and Goalw
1998-06-17, by nipkow
goal -> Goal
1998-06-17, by nipkow
Changed and changed back.
1998-06-17, by nipkow
Goals may now contain assumptions, which are not returned.
1998-06-17, by nipkow
added General/history.ML;
1998-06-16, by wenzelm
Histories of values, with undo and redo;
1998-06-16, by wenzelm
use_text replaces use_strings;
1998-06-15, by wenzelm
handle_error: capture error msgs, even if no exception raised;
1998-06-15, by wenzelm
removed use_text;
1998-06-13, by wenzelm
added use_text;
1998-06-12, by wenzelm
Context.add_session;
1998-06-12, by wenzelm
changed (| |) syntax to (: :);
1998-06-12, by wenzelm
changed {: :} syntax to (| |);
1998-06-12, by wenzelm
tuned exports;
1998-06-12, by wenzelm
removed rel.ML
1998-06-11, by nipkow
ancient relic
1998-06-11, by nipkow
Context.the_context;
1998-06-10, by wenzelm
get_context renamed to the_context;
1998-06-10, by wenzelm
tuned transaction;
1998-06-10, by wenzelm
tuned comments;
1998-06-10, by wenzelm
adapted to TheoryDataFun interface;
1998-06-10, by wenzelm
moved attributes theory data to Isar/isar_thy.ML;
1998-06-10, by wenzelm
less
more
|
(0)
-1920
+1920
+10000
+30000
tip