isabelle: Graph

tidied
2003-03-31, by paulson
Margin for pretty-printing is now a mutable reference.
2003-03-29, by berghofe
Proofs for section 4.5.3
2003-03-26, by paulson
Added show_brackets to settings menu.
2003-03-25, by berghofe
Re-structured some proofs in order to get rid of rule_format attribute.
2003-03-25, by berghofe
New theorems split_div' and mod_div_equality'.
2003-03-25, by berghofe
Presburger arithmetic
2003-03-25, by berghofe
Added examples for Presburger arithmetic.
2003-03-25, by berghofe
Added decision procedure for Presburger arithmetic.
2003-03-25, by berghofe
Added Presburger theory.
2003-03-25, by berghofe
Added hook for presburger arithmetic decision procedure.
2003-03-25, by berghofe
New decision procedure for Presburger arithmetic.
2003-03-25, by berghofe
*** empty log message ***
2003-03-23, by nipkow
More on progress sets
2003-03-21, by paulson
quadratic reciprocity files
2003-03-21, by paulson
Gauss, UNITY, ZF
2003-03-20, by paulson
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
2003-03-20, by paulson
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
2003-03-18, by paulson
toggled show_main_goal
2003-03-18, by nipkow
*** empty log message ***
2003-03-18, by nipkow
just a few mods to a few thms
2003-03-17, by nipkow
More "progress set" material
2003-03-17, by paulson
moved one proof, added another
2003-03-17, by paulson
Bugs fixed and operators finprod and finsum.
2003-03-14, by ballarin
more about list_all2
2003-03-14, by kleing
fix for changes in HOL/Hoare/
2003-03-14, by kleing
Proved the main lemma on progress sets
2003-03-14, by paulson
new UN/INT simprules
2003-03-14, by paulson
split_name no longer uses Sign.string_of_typ to encode types, since
2003-03-13, by berghofe
*** empty log message ***
2003-03-11, by nipkow
*** empty log message ***
2003-03-11, by nipkow
*** empty log message ***
2003-03-11, by nipkow
addsplits / delsplits no longer ignore type of constant.
2003-03-11, by berghofe
First distributed version of Group and Ring theory.
2003-03-10, by ballarin
New theory ProgressSets. Definition of closure sets
2003-03-10, by paulson
spelling
2003-03-10, by paulson
new UNITY examples theory
2003-03-06, by paulson
new logical equivalences
2003-03-06, by paulson
new simprule for int (nat n)
2003-03-06, by paulson
link to devel snapshot
2003-03-06, by kleing
obsolete
2003-03-06, by kleing
new examples theory
2003-03-05, by paulson
get cvs to change modified time for session.tex
2003-03-02, by kleing
typo
2003-03-01, by kleing
added exercises
2003-03-01, by kleing
added Exercises
2003-03-01, by kleing
keep a copy of generated files in repository
2003-03-01, by kleing
keep a copy of generated files in repository
2003-03-01, by kleing
generate nightly devel snapshot
2003-02-28, by isatest
case distinction on host for makefile flags
2003-02-28, by isatest
Reorganized, moving many results about the integer dvd relation from IntPrimes
2003-02-27, by paulson
restored some deleted lemmas
2003-02-27, by paulson
Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-27, by ballarin
== -> =
2003-02-26, by kleing
zprime_def fixes by Jeremy Avigad
2003-02-26, by paulson
completed proofs for programs consisting of a single assignment
2003-02-26, by paulson
new lemma
2003-02-26, by paulson
some x-symbols and some new lemmas
2003-02-26, by paulson
*** empty log message ***
2003-02-25, by nipkow
added simp_depth_limit
2003-02-25, by nipkow
Documented prf / full_prf commands and antiquotations.
2003-02-25, by berghofe
Undid eta change for UN/INT.
2003-02-25, by nipkow
new inverse image lemmas
2003-02-20, by paulson
minor updates to pre-2002 release
2003-02-20, by paulson
fixed anomalies in the installed classical rules
2003-02-19, by paulson
check maxs in defensive machine
2003-02-18, by kleing
new theory Transformers: Meier-Sanders non-interference theory
2003-02-18, by paulson
Proof of the Schorr-Waite graph marking algorithm.
2003-02-17, by mehta
minor revisions
2003-02-16, by paulson
new theorem Compl_partition2
2003-02-16, by paulson
Product operator added --- preliminary.
2003-02-14, by ballarin
favicon
2003-02-12, by kleing
*** empty log message ***
2003-02-11, by nipkow
*** empty log message ***
2003-02-10, by nipkow
New development of algebra: Groups.
2003-02-10, by ballarin
converting HOL/UNITY to use unconditional fairness
2003-02-08, by paulson
adjusted dom rules
2003-02-08, by nipkow
(*f -> ( *f because of new comments
2003-02-07, by nipkow
Removed (*) because of comments
2003-02-07, by nipkow
Added (* ... *) comments in formulae.
2003-02-07, by nipkow
changed ** to ## to avoid conflict with new comment syntax
2003-02-06, by paulson
more tidying
2003-02-05, by paulson
some x-symbols
2003-02-04, by paulson
New tool for displaying version information.
2003-02-03, by berghofe
Fill in version information in lib/Tools/version.
2003-02-03, by berghofe
Added "print_intros" command.
2003-02-03, by berghofe
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
2003-02-03, by berghofe
Moved find_intros_goal from goals.ML to pure_thy.ML
2003-02-03, by berghofe
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
2003-02-03, by berghofe
conversion to new-style theories and tidying
2003-01-31, by paulson
conversion of UNITY theories to new-style
2003-01-30, by paulson
converting more UNITY theories to new-style
2003-01-30, by paulson
Some tuning:
2003-01-29, by berghofe
Added function rev_append.
2003-01-29, by berghofe
Fixed bug in function corr.
2003-01-29, by berghofe
converted more UNITY theories to new-style
2003-01-29, by paulson
*** empty log message ***
2003-01-29, by nipkow
converting UNITY to new-style theories
2003-01-29, by paulson
New example
2003-01-28, by nipkow
pos/neg_mod_sign/bound are now simp rules.
2003-01-28, by nipkow
fixed missing UNITY files
2003-01-27, by kleing
More conversion of UNITY to Isar new-style theories
2003-01-24, by paulson
Partial conversion of UNITY to Isar new-style theories
2003-01-24, by paulson
tidying (by script)
2003-01-23, by paulson
Fixed term order for normal form in rings.
2003-01-23, by ballarin
Added rename_abs attribute for renaming bound variables.
2003-01-17, by berghofe
*** empty log message ***
2003-01-17, by nipkow
more new-style theories
2003-01-15, by paulson
moving "let" from ZF to FOL
2003-01-15, by paulson
auto-update
2003-01-15, by paulson
*** empty log message ***
2003-01-09, by nipkow
New files in Hoare/
2003-01-08, by nipkow
corrected swallowing of newlines after end-of-ignore: rollback
2003-01-08, by oheimb
corrected swallowing of newlines after end-of-ignore (improved)
2003-01-07, by oheimb
new versions of merge-example
2003-01-07, by nipkow
Split Pointers.thy and automated one proof, which caused the runtime to explode
2003-01-06, by nipkow
*** empty log message ***
2003-01-05, by nipkow
*** empty log message ***
2003-01-03, by nipkow
*** empty log message ***
2002-12-30, by nipkow
*** empty log message ***
2002-12-29, by nipkow
*** empty log message ***
2002-12-29, by nipkow
*** empty log message ***
2002-12-29, by nipkow
*** empty log message ***
2002-12-23, by nipkow
removed some problems with print translations
2002-12-22, by nipkow
added print translations tha avoid eta contraction for important binders.
2002-12-22, by nipkow
*** empty log message ***
2002-12-22, by nipkow
*** empty log message ***
2002-12-20, by nipkow
auto-update
2002-12-19, by paulson
*** empty log message ***
2002-12-18, by nipkow
auto-update
2002-12-17, by paulson
new int induction rules
2002-12-17, by paulson
new material for trace_unify_fail
2002-12-17, by paulson
Added mk_int and mk_list.
2002-12-16, by berghofe
Code generator for datatypes now also generates suitable term_of functions (when
2002-12-16, by berghofe
- Added mode reference variable (may be used to switch on and off specific
2002-12-16, by berghofe
cent/currency: changed from wasysym to textcomp because of PDF problems
2002-12-13, by oheimb
trace_unify_fail
2002-12-13, by paulson
integer induction rules
2002-12-13, by paulson
size_of_proof no longer includes size_of_term
2002-12-13, by berghofe
deleted redundant line
2002-12-13, by paulson
Better treatment of equality in premises of inductive definitions. Less
2002-12-12, by paulson
Fixed error that affected document preperation.
2002-12-12, by ballarin
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
2002-12-11, by ballarin
Added size_of_proof.
2002-12-10, by berghofe
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
2002-12-09, by ballarin
corrected swallowing of newlines after end-of-ignore
2002-12-06, by oheimb
*** empty log message ***
2002-12-06, by nipkow
for dvi target
2002-12-05, by kleing
exercise collection
2002-12-05, by kleing
Incompatibility with SML/NJ fixed.
2002-11-29, by ballarin
added a few lemmas
2002-11-29, by nipkow
Transitivity reasoner renamed to linorder.ML. README updated.
2002-11-28, by ballarin
HOL-Algebra partially ported to Isar.
2002-11-28, by ballarin
prop_of now returns proposition in beta-eta normal form.
2002-11-27, by berghofe
- tuned beta_eta_convert
2002-11-27, by berghofe
Correctness proofs are now modular, too.
2002-11-27, by berghofe
Parameters in definitions are now renamed to avoid clashes with
2002-11-27, by berghofe
default_output now escapes \'s more carefully.
2002-11-27, by berghofe
Added XML parser (useful for parsing PGIP / PGML).
2002-11-27, by berghofe
Added some functions for processing PGIP (thanks to David Aspinall).
2002-11-27, by berghofe
Fixed bug in consts_code section.
2002-11-27, by berghofe
Replaced some blasts by rules.
2002-11-27, by berghofe
Changed format of realizers / correctness proofs.
2002-11-27, by berghofe
renamed a few constants
2002-11-25, by nipkow
*** empty log message ***
2002-11-21, by nipkow
textual tweak
2002-11-20, by paulson
stylistic tweaks
2002-11-19, by paulson
beautification
2002-11-18, by nipkow
Fixed small bug that caused some definitions to be "forgotten".
2002-11-17, by berghofe
beautified "match"
2002-11-16, by kleing
beautified "match"
2002-11-16, by kleing
added zdvd_iff_zmod_eq_0
2002-11-15, by nipkow
Improved function decompose.
2002-11-13, by berghofe
- exported functions etype_of and mk_typ
2002-11-13, by berghofe
Fixed name clash problem in forall_elim_var.
2002-11-13, by berghofe
Added simple_prove_goal_cterm.
2002-11-13, by berghofe
Removed (now unneeded) declarations of realizers for bar induction.
2002-11-13, by berghofe
New package for constructing realizers for introduction and elimination
2002-11-13, by berghofe
- No longer applies norm_hhf_rule
2002-11-13, by berghofe
prove_goal' -> Goal.simple_prove_goal_cterm
2002-11-13, by berghofe
name_of_type now replaces non-identifiers by dummy names.
2002-11-13, by berghofe
Added inductive_realizer.
2002-11-13, by berghofe
Added InductiveRealizer package.
2002-11-13, by berghofe
Transitive closure is now defined inductively as well.
2002-11-13, by berghofe
Hoare.ML -> hoare.ML
2002-11-09, by kleing
Polishing.
2002-11-08, by paulson
generalized wf_on_unit to wf_on_any_0
2002-11-08, by paulson
added raw proof blocks
2002-11-07, by nipkow
small improvements
2002-11-07, by nipkow
added show_main_goal
2002-11-07, by nipkow
Hoare.ML -> hoare.ML
2002-11-06, by nipkow
a new pointer example and some syntactic sugar
2002-11-06, by nipkow
two new Bali files
2002-11-05, by kleing
new operator transrec3
2002-11-05, by paulson
Removed obsolete section about reordering assumptions.
2002-11-04, by berghofe
proof streamlining
2002-11-01, by paulson
tidy
2002-11-01, by paulson
Inserted some extra paragraphs in large proofs to make tex run...
2002-11-01, by schirmer
fixed "latex capacity exceeded"
2002-11-01, by kleing
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
2002-10-31, by schirmer
simpler separation/replacement proofs
2002-10-30, by paulson
modified msg
2002-10-30, by nipkow
added induction thms
2002-10-29, by nipkow
moved fac example
2002-10-28, by nipkow
*** empty log message ***
2002-10-28, by nipkow
conversion ML -> thy
2002-10-28, by nipkow
simplified lemma correct_frames_newref
2002-10-27, by kleing
switched to atbroy51, removed markus from email list
2002-10-26, by isatest
fixed latex output
2002-10-25, by kleing
changes for cleanup in JVM
2002-10-24, by kleing
cleanup, beautified
2002-10-24, by kleing
fixed latex error
2002-10-24, by kleing
ASIN -> SET
2002-10-24, by nipkow
*** empty log message ***
2002-10-23, by streckem
First checkin of compiler
2002-10-23, by streckem
Added compiler
2002-10-23, by streckem
Eta contraction is now switched off when printing extracted program.
2002-10-21, by berghofe
Fixed problem with theorems containing TFrees.
2002-10-21, by berghofe
- reconstruct_proof no longer relies on TypeInfer.infer_types
2002-10-21, by berghofe
Removed Logic.skip_flexpairs.
2002-10-21, by berghofe
Replaced variantlist (quadratic) by gen_names (linear).
2002-10-21, by berghofe
Removed add_env because Vartab.map was too slow for large environments.
2002-10-21, by berghofe
- removed flexpair
2002-10-21, by berghofe
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
2002-10-21, by berghofe
Removed flexpair_def.
2002-10-21, by berghofe
Removed Logic.strip_flexpairs.
2002-10-21, by berghofe
No more explicit manipulation of flex-flex constraints in goals_conv.
2002-10-21, by berghofe
Changed type of Logic.strip_horn.
2002-10-21, by berghofe
Removed obsolete functions dealing with flex-flex constraints.
2002-10-21, by berghofe
Changed handling of flex-flex constraints: now stored in separate
2002-10-21, by berghofe
Now applies standard' to "unfold" theorem (due to flex-flex constraints).
2002-10-21, by berghofe
Changed type of Logic.strip_horn.
2002-10-21, by berghofe
Tidying up. New primitives is_iterates and is_iterates_fm.
2002-10-18, by paulson
Mod due to: Added a few thms about UN/INT/{}/UNIV
2002-10-18, by nipkow
Added a few thms about UN/INT/{}/UNIV
2002-10-18, by nipkow
fixed comments and types
2002-10-17, by paulson
Cosmetic changes suggested by writing the paper. Deleted some
2002-10-17, by paulson
fixing the cut_tac method to work when there are no instantiations and the
2002-10-17, by paulson
alternative syntax
2002-10-15, by kleing
*** empty log message ***
2002-10-14, by nipkow