isabelle: Graph

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