isabelle: Graph

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
tidying and reorganization
2002-10-14, by paulson
Ported find_intro/elim to Isar.
2002-10-14, by nipkow
norm_typ -> Envir.norm_type
2002-10-11, by berghofe
*** empty log message ***
2002-10-10, by nipkow
*** empty log message ***
2002-10-10, by nipkow
added failure trace information to pattern unification
2002-10-10, by nipkow
Reimplemented parts of datatype package dealing with datatypes involving
2002-10-10, by berghofe
Added list_all.
2002-10-10, by berghofe
Removed obsolete function "fun_rel_comp".
2002-10-10, by berghofe
Added choice_eq.
2002-10-10, by berghofe
- Added range_ex1_eq
2002-10-10, by berghofe
Removed obsolete function "Funs".
2002-10-10, by berghofe
Added functions Suml and Sumr which are useful for constructing
2002-10-10, by berghofe
Re-organization of Constructible theories
2002-10-09, by paulson
type safety with defensive machine
2002-10-08, by kleing
defensive machine
2002-10-08, by kleing
defensive machine without obj init and jsr
2002-10-08, by kleing
Got rid of rotates because of new simplifier
2002-10-08, by nipkow
take/drop -> splitAt
2002-10-07, by nipkow
Various simplifications of the Constructible theories
2002-10-04, by paulson
Fixed bug involving inductive definitions with equalities in the premises.
2002-10-04, by paulson
Fixed bug involving inductive definitions having equalities in the premises,
2002-10-04, by paulson
Documented new "asm_lr" option for simp.
2002-10-04, by berghofe
added the new elim rule psubsetE
2002-10-03, by paulson
*** empty log message ***
2002-10-03, by nipkow
*** empty log message ***
2002-10-02, by nipkow
*** empty log message ***
2002-10-02, by nipkow
*** empty log message ***
2002-10-02, by nipkow
*** empty log message ***
2002-10-01, by nipkow
Added some comments on new simplifier.
2002-10-01, by berghofe
Documented new "asm_lr" option for simp.
2002-10-01, by berghofe
Adapted to new simplifier.
2002-10-01, by berghofe
Numerous cosmetic changes, prompted by the new simplifier
2002-10-01, by paulson
Deleted superfluous dest_implies.
2002-10-01, by berghofe
*** empty log message ***
2002-09-30, by nipkow
Adapted to new simplifier.
2002-09-30, by berghofe
Adapted to new simplifier.
2002-09-30, by berghofe
Fixed bug in expand_proof which caused indexes to be incremented incorrectly.
2002-09-30, by berghofe
Added check for axioms with "realizes Null A = A".
2002-09-30, by berghofe
Added function elim_vars.
2002-09-30, by berghofe
Completely reimplemented mutual simplification of premises.
2002-09-30, by berghofe
Removed nRS again because extract_rews now takes care of preserving names.
2002-09-30, by berghofe
Added syntax for "asm_lr" simplifier option.
2002-09-30, by berghofe
- eliminated thin_leading_eqs_tac
2002-09-30, by berghofe
Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
2002-09-30, by berghofe
- additional congruence rules for boolean operators
2002-09-30, by berghofe
Adapted to new simplifier.
2002-09-30, by berghofe
Removed nRS again because extract_rews now takes care of preserving names.
2002-09-30, by berghofe
Added elim_vars to preprocessor.
2002-09-30, by berghofe
Fixed problem with induct_conj_curry: variable C should have type prop.
2002-09-30, by berghofe
fixes !!-bound vars in induction statement automatically
2002-09-30, by nipkow
modified induct method
2002-09-30, by nipkow
Proof tidying
2002-09-27, by paulson
Isar experiments, etc.
2002-09-27, by paulson
Tidied. New Pi-theorem.
2002-09-27, by paulson
new Ring example
2002-09-27, by paulson
Isar proof
2002-09-27, by paulson
Modules theory added
2002-09-27, by paulson
New theory GroupTheory/Module.thy of modules
2002-09-27, by paulson
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
2002-09-26, by paulson
GroupTheory and FuncSet
2002-09-26, by paulson
new theory for Pi-sets, restrict, etc.
2002-09-26, by paulson
Converted Fun to Isar style.
2002-09-26, by paulson
new document directory for GroupTheory
2002-09-26, by paulson
converted to Isar and using new "implicit structures" instead of Sigma, etc
2002-09-26, by paulson
*** empty log message ***
2002-09-25, by nipkow
*** empty log message ***
2002-09-25, by nipkow
*** empty log message ***
2002-09-25, by nipkow
Int.thy -> int.thy
2002-09-25, by nipkow
became int.ML
2002-09-25, by nipkow
conversion to Isar
2002-09-25, by nipkow
converted to Isar
2002-09-25, by nipkow
added nat_split
2002-09-25, by nipkow
converted to Isar script
2002-09-21, by paulson
shortened a proof
2002-09-20, by paulson
got rid of deepen_tac
2002-09-20, by paulson
less use of x-symbols
2002-09-20, by paulson
*** empty log message ***
2002-09-19, by nipkow
drule: added nRS
2002-09-19, by nipkow
preserve names of rewrite rules when transforming them
2002-09-19, by nipkow
comments + usage
2002-09-18, by kleing
Streamlined proofs of instances of Separation
2002-09-11, by paulson
Bound variable preservation in Collect_cong
2002-09-11, by paulson
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
2002-09-10, by paulson
tweaks
2002-09-10, by paulson
*** empty log message ***
2002-09-09, by nipkow
bug in counter example finder
2002-09-09, by nipkow
conversion of ZF/Integ/{Int,Bin} to Isar scripts
2002-09-07, by paulson
added checking so that (rename_tac "x y") is rejected, since
2002-09-05, by paulson
tidied
2002-09-03, by paulson
deleted redundant material (quasiformula, ...) and rationalized
2002-09-03, by paulson
fixed the typesetting
2002-09-03, by paulson
*** empty log message ***
2002-09-03, by nipkow
Added missing rewrite rule and some arith examples
2002-09-02, by paulson
order_less_irrefl: [simp] -> [iff]
2002-09-02, by nipkow
*** empty log message ***
2002-09-01, by nipkow
converted Hyperreal/Zorn to Isar format and moved to Library
2002-08-31, by paulson
removal of blast.overloaded
2002-08-30, by paulson
updated;
2002-08-29, by wenzelm
*** empty log message ***
2002-08-29, by wenzelm
tuned;
2002-08-29, by wenzelm
fixed a name clash
2002-08-29, by paulson
improved tell_thm_deps;
2002-08-28, by wenzelm
various new lemmas for Constructible
2002-08-28, by paulson
completion of the consistency proof for AC
2002-08-28, by paulson
thms_containing: allow "_" in specification;
2002-08-27, by wenzelm
*** empty log message ***
2002-08-27, by wenzelm