isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

New example ported from ZF
1997-05-26, by paulson
Simplified proofs using expand_option_case
1997-05-26, by paulson
Now checks the name of the function being defined;
1997-05-26, by paulson
More de-HOL-ification
1997-05-26, by paulson
Now checks the name of the function being defined
1997-05-26, by paulson
Deleted unused functions
1997-05-26, by paulson
Now a Perl script. No longer requires commands to be at the beginnings of
1997-05-26, by paulson
Slight simplifications
1997-05-26, by paulson
Eliminated ccc1. Moved ID,oo into Cfun.
1997-05-25, by slotosch
Moved the classes flat chfin from Fix to Pcpo.
1997-05-25, by slotosch
*** empty log message ***
1997-05-25, by slotosch
Eliminated the prediates flat,chfin
1997-05-25, by slotosch
eliminated the constant less by the introduction of the axclass sq_ord
1997-05-25, by slotosch
tuned;
1997-05-23, by wenzelm
arbitrary
1997-05-23, by nipkow
Added `arbitrary'
1997-05-23, by nipkow
fixed;
1997-05-23, by wenzelm
new syntactic priority of lambda abstraction
1997-05-23, by oheimb
adapted entry for addss, addSss
1997-05-23, by oheimb
news.
1997-05-23, by nipkow
Documented `size' function for datatypes.
1997-05-23, by nipkow
fixed a bug
1997-05-23, by mueller
removed TFL from test;
1997-05-23, by wenzelm
remove cl.cam font server;
1997-05-23, by wenzelm
exec the emacs;
1997-05-23, by wenzelm
Base theory is now Arith, not Nat. (because all datatypes now require Arith).
1997-05-23, by nipkow
All datatypes now require Arith.
1997-05-23, by nipkow
Added overloaded function `size' for all datatypes.
1997-05-23, by nipkow
exhaust_tac can now deal with whole terms rather than just variables.
1997-05-22, by nipkow
added href to Isamode;
1997-05-22, by wenzelm
fixed doc;
1997-05-22, by wenzelm
adapted to Isamode 2.6;
1997-05-22, by wenzelm
tuned Isamode stuff;
1997-05-22, by wenzelm
New headers and other minor changes
1997-05-22, by paulson
Now the recdef induction rule variables are named u, v, ...
1997-05-22, by paulson
New example of recdef and permutative rewriting
1997-05-22, by paulson
Now uses type option instead of Fail/Subst
1997-05-22, by paulson
Now uses type option instead of Fail/Subst
1997-05-22, by paulson
Uses option_case_tac
1997-05-22, by paulson
Deleted rprod: lex_prod is (usually?) enough
1997-05-22, by paulson
Deleted obsolete proofs. But option_case_tac will be obsolete too
1997-05-22, by paulson
New example: ex/Fib
1997-05-22, by paulson
New lemmas used for ex/Fib
1997-05-22, by paulson
Added rotation to exhaust_tac.
1997-05-22, by nipkow
tuned;
1997-05-22, by wenzelm
added;
1997-05-22, by wenzelm
tuned;
1997-05-22, by wenzelm
SYNC;
1997-05-22, by wenzelm
Documented exhaust_tac.
1997-05-22, by nipkow
fixed packages;
1997-05-22, by wenzelm
fixed packages;
1997-05-22, by wenzelm
tuned comments;
1997-05-22, by wenzelm
Replaced res_inst-list_cases by generic exhaust_tac.
1997-05-22, by nipkow
Added exhaustion thm and exhaust_tac for each datatype.
1997-05-22, by nipkow
fixed find cmd;
1997-05-21, by wenzelm
set version;
1997-05-21, by wenzelm
tuned all READMEs;
1997-05-21, by wenzelm
release version (sort of);
1997-05-21, by wenzelm
SYNC;
1997-05-21, by wenzelm
fixed spelling;
1997-05-21, by wenzelm

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

isabelle