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

generate devel snapshot even if experimental builds fail.
2006-10-15, by kleing
added peek;
2006-10-14, by wenzelm
added theorem(_i);
2006-10-14, by wenzelm
export map_elem;
2006-10-14, by wenzelm
added assert;
2006-10-14, by wenzelm
theorem: added local_theory version;
2006-10-14, by wenzelm
Attrib.pretty_attrib;
2006-10-14, by wenzelm
added pretty_attribs (from attrib.ML);
2006-10-14, by wenzelm
moved pretty_attribs to attrib.ML;
2006-10-14, by wenzelm
locale begin/end;
2006-10-14, by wenzelm
updated;
2006-10-13, by wenzelm
Added keywords for new inductive definition package.
2006-10-13, by berghofe
Adapted to changes in FixedPoint theory.
2006-10-13, by berghofe
Moved old inductive package to old_inductive_package.ML
2006-10-13, by berghofe
Completely rewrote inductive definition package. Now allows to
2006-10-13, by berghofe
Old version of inductive definition package (for sets).
2006-10-13, by berghofe
Moved old inductive package to old_inductive_package.ML
2006-10-13, by berghofe
Adapted to new inductive definition package.
2006-10-13, by berghofe
Adapted to changes in FixedPoint theory.
2006-10-13, by berghofe
Legacy ML bindings now refer to old inductive definition package.
2006-10-13, by berghofe
Added new package for inductive definitions, moved old package
2006-10-13, by berghofe
Generalized gfp and lfp to arbitrary complete lattices.
2006-10-13, by berghofe
Repaired strip_assums_hyp (now also works for goals not
2006-10-13, by berghofe
improved framework
2006-10-13, by haftmann
refined
2006-10-13, by haftmann
fixed bug
2006-10-13, by haftmann
tuned
2006-10-13, by haftmann
added codegen2 example
2006-10-13, by haftmann
added the missing freshness-lemmas for nat, int, char and string and
2006-10-13, by urbanc
lifted claset setup from ML to Isar level
2006-10-13, by haftmann
explicit nonfix for union and inter
2006-10-13, by haftmann
renamed enter_forward_proof to enter_proof_body;
2006-10-12, by wenzelm
added peek;
2006-10-12, by wenzelm
interpretation_in_locale: standalone goal setup;
2006-10-12, by wenzelm
tuned;
2006-10-12, by wenzelm
renamed print_lthms to print_facts, do not insist on proof state;
2006-10-12, by wenzelm
print_evaluated_term: Toplevel.context_of;
2006-10-12, by wenzelm
replaced attributes_update by map_attributes;
2006-10-12, by wenzelm
Toplevel.local_theory_to_proof: proper target;
2006-10-12, by wenzelm
Toplevel.local_theory: proper target;
2006-10-12, by wenzelm
To be consistent with "induct", I renamed "fixing" to "arbitrary".
2006-10-12, by urbanc
Extended combinators now disabled
2006-10-12, by paulson
abstraction is now turned OFF...
2006-10-12, by paulson
Logging of theorem names to the /tmp directory now works
2006-10-12, by paulson
cc: avoid space after options;
2006-10-12, by wenzelm
set DYLD_LIBRARY_PATH (for Darwin);
2006-10-12, by wenzelm
added execute/system;
2006-10-12, by wenzelm
added x86-darwin;
2006-10-12, by wenzelm
now allowing subdirectories in Doc/
2006-10-12, by haftmann
added makefile layer
2006-10-12, by haftmann
* isabelle-process: option -S (secure mode) disables some critical operations;
2006-10-11, by wenzelm
increased heap size for polyml-4.9.1;
2006-10-11, by wenzelm
tuned Toplevel.begin_local_theory;
2006-10-11, by wenzelm
exit_local_theory: pass interactive flag;
2006-10-11, by wenzelm
exit: pass interactive flag;
2006-10-11, by wenzelm
added begin parser;
2006-10-11, by wenzelm
is_sid: disallow 'begin' keyword as identifier;
2006-10-11, by wenzelm
exit: pass interactive flag, toplevel result convention;
2006-10-11, by wenzelm
add_defs: declare terms;
2006-10-11, by wenzelm
'context': demand 'begin', support local theory;
2006-10-11, by wenzelm

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

isabelle