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

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
removed 'undo_end', recovered 'cannot_undo';
2006-10-11, by wenzelm
tuned signature;
2006-10-11, by wenzelm
minor refinements in serialization
2006-10-11, by haftmann
adapted to signature change
2006-10-11, by haftmann
slight type signature changes
2006-10-11, by haftmann
cleaned up HOL bootstrap
2006-10-11, by haftmann
abandoned findrep
2006-10-11, by haftmann
added code generator setup
2006-10-11, by haftmann
added code lemma
2006-10-11, by haftmann
Abstraction re-use code now checks that the abstraction function can be used in the current
2006-10-11, by paulson
added examples for nested let
2006-10-11, by haftmann
added tex files to CVS
2006-10-11, by haftmann
renamed body_context_node to presentation_context;
2006-10-11, by wenzelm
add_locale(_i): return actual result context;
2006-10-11, by wenzelm
class(_i): mimic Locale.add_locale(_i);
2006-10-11, by wenzelm
added type global_theory -- theory or local_theory;
2006-10-11, by wenzelm
added begin;
2006-10-11, by wenzelm
added opt_begin;
2006-10-11, by wenzelm
added raw_theory(_result);
2006-10-11, by wenzelm

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

isabelle