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

Contents: suppress comments;
2000-01-17, by wenzelm
Thm.instantiate no longer normalizes, but Drule.instantiate does
2000-01-17, by paulson
still working; a bit of polishing
2000-01-14, by paulson
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
2000-01-13, by paulson
change for new rewriting
2000-01-13, by paulson
added recursor
2000-01-13, by paulson
change in add_thmss to suppress warning
2000-01-13, by paulson
a bit of tidying
2000-01-13, by paulson
working version, with Alloc now working on the same state space as the whole
2000-01-13, by paulson
new theorem subset_Compl_self_eq
2000-01-13, by paulson
tuned comment;
2000-01-13, by wenzelm
Move some lemmas to List.
2000-01-12, by nipkow
More lemmas.
2000-01-12, by nipkow
isabellesimple: avoid paragraph;
2000-01-10, by wenzelm
int:nat->int is pushed inwards.
2000-01-10, by nipkow
Forgot to "call" MicroJava in makefile.
2000-01-10, by nipkow
tidied parentheses
2000-01-07, by paulson
tidied
2000-01-07, by paulson
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
2000-01-07, by paulson
better automation for "slice"
2000-01-07, by paulson
moved some proofs from UNITY/ELT to UNITY/Project
2000-01-07, by paulson
obtain: renamed 'in' to 'where';
2000-01-06, by wenzelm
oops';
2000-01-05, by wenzelm
oops;
2000-01-05, by wenzelm
improved symbol for subcls relation
2000-01-05, by oheimb
simplified definition of appl_methds, removing m_head
2000-01-05, by oheimb
tuned;
2000-01-05, by wenzelm
obtain;
2000-01-05, by wenzelm
comment: any number of texts;
2000-01-05, by wenzelm
proof markup: any mode;
2000-01-05, by wenzelm
replaced HOLogic.termTVar by HOLogic.termT;
2000-01-05, by wenzelm
ObtainFun;
2000-01-05, by wenzelm
METHOD_CLASET': refer to *local* claset;
2000-01-05, by wenzelm
moved obtain to obtain.ML;
2000-01-05, by wenzelm
TypeInfer.logicT;
2000-01-05, by wenzelm
tuned;
2000-01-05, by wenzelm
ObtainFun;
2000-01-05, by wenzelm
added thms_ctxt_args;
2000-01-05, by wenzelm
prepare patterns only once;
2000-01-05, by wenzelm
ObtainFun;
2000-01-05, by wenzelm
present chapter;
2000-01-05, by wenzelm
removed pats;
2000-01-05, by wenzelm
chapter;
2000-01-05, by wenzelm
support for dummy variables (anyT, logicT);
2000-01-05, by wenzelm
TypeInfer.logicT;
2000-01-05, by wenzelm
new arg type for max_spec etc.
2000-01-04, by oheimb
small changes;
2000-01-03, by bauerg
removed inj_eq from the default simpset again
2000-01-03, by oheimb
removed inj_eq from the default simpset again
2000-01-03, by oheimb
removed inj_eq from the default simpset again
1999-12-23, by oheimb
updated sml package name in installation exmaple
1999-12-23, by kleing
raw_t(e)xt: any proof mode;
1999-12-22, by wenzelm
fixed error msg;
1999-12-22, by wenzelm
marg_comment: repeat;
1999-12-22, by wenzelm
text: string list;
1999-12-22, by wenzelm
tidied, with a bit more progress
1999-12-22, by paulson
Working version after a FAILED attempt to base Follows upon LeadsETo
1999-12-22, by paulson
new weakening laws
1999-12-22, by paulson
removing the "{} : CC" requirement for leadsTo[CC]
1999-12-22, by paulson
back to old sml version (due to c library problems)
1999-12-22, by kleing

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

isabelle