isabelle: Graph

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

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
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
Toplevel.end_proof;
2006-10-11, by wenzelm
'end': handle local theory;
2006-10-11, by wenzelm
undo_end/kill: handle local theory;
2006-10-11, by wenzelm
Toplevel: generic_theory;
2006-10-11, by wenzelm
made some proof look more like the ones in Barendregt
2006-10-10, by urbanc
A way to call the ATP linkup from ML scripts
2006-10-10, by paulson
Combinators require the theory name; added settings for SPASS
2006-10-10, by paulson
stripped pointless head
2006-10-10, by haftmann
gen_rem(s) abandoned in favour of remove / subtract
2006-10-10, by haftmann
added IsarAdvanced material
2006-10-10, by haftmann
Induction rules have schematic variables again.
2006-10-10, by krauss
initial draft
2006-10-10, by haftmann
*** empty log message ***
2006-10-10, by haftmann
initial draft
2006-10-10, by haftmann
fixed intendation
2006-10-10, by haftmann
cleanup basic HOL bootstrap
2006-10-10, by haftmann
added legacy tactic
2006-10-10, by haftmann
purged some ML legacy
2006-10-10, by haftmann
added eq_True eq_False True_implies_equals to extraction_expand
2006-10-10, by haftmann
no breaks for Haskell
2006-10-10, by haftmann
removed experimental codegen_simtype
2006-10-10, by haftmann
added keeping of funcgr
2006-10-10, by haftmann
generalized purge
2006-10-10, by haftmann
changed order
2006-10-10, by haftmann
removed quote in serialization
2006-10-10, by haftmann
added code_abstype
2006-10-10, by haftmann
added code_constsubst
2006-10-10, by haftmann
fixed typo
2006-10-10, by haftmann
added code_abstype and code_constsubst
2006-10-10, by haftmann
isabelle-process: options -S, -X;
2006-10-09, by wenzelm
tuned;
2006-10-09, by wenzelm
loop: disallow exit in secure mode;
2006-10-09, by wenzelm
Secure.commit;
2006-10-09, by wenzelm
moved Context.ml_output to Output.ml_output;
2006-10-09, by wenzelm
Secure critical operations.
2006-10-09, by wenzelm
added General/secure.ML;
2006-10-09, by wenzelm
added option -S (secure mode);
2006-10-09, by wenzelm
added nbe_post for delayed_if
2006-10-09, by nipkow
added delayed_if
2006-10-09, by nipkow
added pre/post-processor equations
2006-10-09, by nipkow
attribute "symmetric": standardized schematic variables;
2006-10-09, by wenzelm
sequential lemmas;
2006-10-09, by wenzelm
reorderd ML/lemmas (Why!?);
2006-10-09, by wenzelm
PureThy.note_thmss_i;
2006-10-09, by wenzelm
added exit;
2006-10-09, by wenzelm
added theorems(_i) -- with present_results;
2006-10-09, by wenzelm
def(_i): LocalDefs.add_defs;
2006-10-09, by wenzelm
attribute: Context.mapping;
2006-10-09, by wenzelm
removed obsolete note_thmss(_i);
2006-10-09, by wenzelm
added exit;
2006-10-09, by wenzelm
simplified derived_def;
2006-10-09, by wenzelm