isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip

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

less more | (0) -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle