isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

Direct priority and tracing channels properly.
2007-07-18, by aspinall
tidying using metis
2007-07-18, by paulson
fileident --- produce file identification based;
2007-07-17, by wenzelm
added ISABELLE_FILE_IDENT (command line for source file identification);
2007-07-17, by wenzelm
adapted TextIO.inputLine;
2007-07-17, by wenzelm
tuned comment;
2007-07-17, by wenzelm
avoid redundant variables in patterns (which made Alice vomit);
2007-07-17, by wenzelm
Full sort information by default.
2007-07-17, by paulson
Added hypotheses.
2007-07-17, by berghofe
Added clause for hypotheses to proof_of_xml function.
2007-07-17, by berghofe
use /usr/proj/polyml/polyml-5.1-test, which might be more stable;
2007-07-17, by wenzelm
reverted fun->recdef, since there are problems with induction rule
2007-07-17, by krauss
Pure theory setup.
2007-07-17, by wenzelm
Generic print mode.
2007-07-17, by wenzelm
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
2007-07-17, by wenzelm
simplified loading of ML files -- no static forward references;
2007-07-17, by wenzelm
moved print_translations from Pure.thy to Syntax/syn_trans.ML;
2007-07-17, by wenzelm
added General/print_mode.ML, pure_setup.ML;
2007-07-17, by wenzelm
tuned specifications;
2007-07-17, by wenzelm
use function package
2007-07-16, by krauss
more proofs
2007-07-16, by krauss
some interface cleanup
2007-07-16, by krauss
added lemma binding: accpI = accp.accI
2007-07-16, by krauss
updated
2007-07-16, by krauss
tidied using sledgehammer
2007-07-16, by paulson
tidied
2007-07-16, by paulson
tidied using sledgehammer
2007-07-16, by paulson
tidied using sledgehammer
2007-07-16, by paulson
clarified structure names
2007-07-16, by haftmann
added function for case certificates
2007-07-16, by haftmann
dropped outer ROOT structure for generated code
2007-07-16, by haftmann
tuned
2007-07-16, by haftmann
fixed SML/NJ int problem
2007-07-16, by haftmann
updated
2007-07-16, by haftmann
tuned;
2007-07-13, by wenzelm
updated
2007-07-12, by krauss
updated;
2007-07-12, by wenzelm
tuned signature;
2007-07-12, by wenzelm
sys_error;
2007-07-12, by wenzelm
simplified using Markup.get_int;
2007-07-12, by wenzelm
added skeleton for print_mode setup;
2007-07-12, by wenzelm
tuned spacing;
2007-07-12, by wenzelm
renamed PgipParser to OldPgipParser;
2007-07-12, by wenzelm
Parsing theory sources without execution (via keyword classification).
2007-07-12, by wenzelm
exported command_keyword;
2007-07-12, by wenzelm
command 'declare': proper thy_decl;
2007-07-12, by wenzelm
added get_string, get_int;
2007-07-12, by wenzelm
added ProofGeneral/pgip_parser.ML;
2007-07-12, by wenzelm
tuned error faces;
2007-07-11, by wenzelm
tries to solve goal via TrueI
2007-07-11, by nipkow
tuned markup;
2007-07-11, by wenzelm
replaced OuterLex.name_of by more sophisticated OuterLex.text_of;
2007-07-11, by wenzelm
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-11, by wenzelm
Buffer.markup;
2007-07-11, by wenzelm
removed ident, space;
2007-07-11, by wenzelm
added markup operation;
2007-07-11, by wenzelm
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-11, by wenzelm
Added entry for new inductive definition package.
2007-07-11, by berghofe
Proof terms for meta-conjunctions are now normalized before
2007-07-11, by berghofe
Added function norm_proof for normalizing the proof term
2007-07-11, by berghofe

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

isabelle