isabelle: Graph

interpreter for Finite_Set.Finites added
2005-03-03, by webertj
Move towards standard functions.
2005-03-03, by skalberg
fixed proof
2005-03-03, by nipkow
converted to new-style theory
2005-03-03, by huffman
converted to new-style theory
2005-03-03, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
another reorganization of setsums and intervals
2005-03-02, by nipkow
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
2005-03-02, by dixon
obscured the e-mail address lcp@cl
2005-03-02, by paulson
new lemmas int_diff_cases
2005-03-02, by paulson
eliminated deps for removed files
2005-03-02, by huffman
merged into Discrete.thy
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
integrated Jeremy's FiniteLib
2005-03-01, by nipkow
spider dogding
2005-03-01, by kleing
added setsum_diff1' which holds in more general cases than setsum_diff1
2005-02-28, by obua
unfold theorems for trancl and rtrancl
2005-02-28, by paulson
lucas - added more comments and an extra type to clarify the code.
2005-02-27, by dixon
Modified node_trans to avoid duplication of signature stamps
2005-02-23, by berghofe
exception SAME removed
2005-02-23, by webertj
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
2005-02-23, by webertj
suminf -> \<Sum>
2005-02-23, by nipkow
Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
2005-02-22, by dixon
removed redundant lemmas and simprules
2005-02-22, by paulson
more setsum tuning
2005-02-22, by nipkow
more fine tuniung
2005-02-21, by nipkow
fixed proof
2005-02-21, by nipkow
removed superfluous setsum_constant
2005-02-21, by nipkow
comprehensive cleanup, replacing sumr by setsum
2005-02-21, by nipkow
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
2005-02-19, by dixon
continued eliminating sumr
2005-02-18, by nipkow
starting to get rid of sumr
2005-02-18, by nipkow
tuning
2005-02-18, by nipkow
*** empty log message ***
2005-02-16, by nipkow
refine now provides specific cases "goal1" ... "goaln" for addressing
2005-02-15, by berghofe
simplified a proof
2005-02-14, by paulson
Deleted Library.option type.
2005-02-13, by skalberg
Fully qualified refl and trans to avoid confusion with theorems
2005-02-11, by berghofe
Optimized present_tokens to produce fewer newlines when hiding proofs.
2005-02-11, by berghofe
New reference Toplevel.debug for verbose printing of exns.
2005-02-11, by ballarin
update from Larry
2005-02-11, by kleing
some stuff is now redundant.
2005-02-10, by nipkow
HOL.order -> Orderings.order due to restructering
2005-02-10, by nipkow
Moved oderings from HOL into the new Orderings.thy
2005-02-10, by nipkow
Added paper by M. Takahashi.
2005-02-10, by berghofe
Added proof of eta-postponement theorem (using parallel eta-reduction).
2005-02-10, by berghofe
non-inductive fold1Set proofs
2005-02-10, by paulson
simplified a key lemma for foldSet
2005-02-10, by paulson
Toplevel.debug for debugging in Isar.
2005-02-10, by ballarin
Fixed bug in select_thm.
2005-02-10, by berghofe
Subscripts for theorem lists now start at 1.
2005-02-10, by berghofe
mention authors are acknowledged for isabelle-lemmas
2005-02-10, by kleing
more preview
2005-02-10, by kleing
pointer to isabelle-lemmas submission list
2005-02-10, by kleing
added lattice_locales
2005-02-09, by nipkow
Extracted generic lattice stuff to new Lattice_Locales.thy
2005-02-09, by nipkow
New
2005-02-09, by nipkow
new foldSet proofs
2005-02-09, by paulson
revised fold1 proofs
2005-02-09, by paulson
revised fold1 proofs
2005-02-09, by paulson
cvs merge problem fixed
2005-02-08, by nipkow
new treatment of fold1
2005-02-08, by paulson
Fixed lattice defns
2005-02-08, by nipkow
*** empty log message ***
2005-02-07, by nipkow
fixed latex problems by including bigsqcap
2005-02-07, by nipkow
fixed latex problems
2005-02-07, by nipkow
fixed mac line
2005-02-06, by paulson
Added Lattice locale
2005-02-05, by nipkow
clausification and proof reconstruction
2005-02-04, by paulson
comment
2005-02-04, by paulson
Added semi-lattice locales and reorganized fold1 lemmas
2005-02-04, by nipkow
added find_rewrites
2005-02-03, by nipkow
new treatment of demodulation in proof reconstruction
2005-02-03, by paulson
don't generate latex for LaTeXsugar and OptionalSugar
2005-02-03, by kleing
removed sugar.sty (obsolete for devel version)
2005-02-03, by kleing
not needed any more by LaTeXSugar
2005-02-03, by kleing
Document now applies to devel version (and Isabelle 2005)
2005-02-03, by kleing
Replaced application of subst by simplesubst in proof of app_Var_NF
2005-02-02, by berghofe
Replaced application of subst by simplesubst in proof of rev_induct
2005-02-02, by berghofe
tidying of some subst/simplesubst proofs
2005-02-02, by paulson
generalization and tidying
2005-02-02, by paulson
improved handling of chained facts
2005-02-02, by paulson
Max_le -> Max_ge
2005-02-02, by nipkow
fold and fol1 changes
2005-02-02, by nipkow
added [simp]
2005-02-02, by nipkow
link to PG FAQ for start up problem
2005-02-02, by kleing
the new subst tactic, by Lucas Dixon
2005-02-01, by paulson
renamed a few vars, added a lemma
2005-01-30, by nipkow
proof simpification
2005-01-28, by nipkow
moved sugar.sty to textinputs
2005-01-28, by kleing
-H false for showing proofs (not -H true)
2005-01-28, by kleing
fixed bugs
2005-01-27, by nipkow
- Proofs are now hidden by default when generating documents
2005-01-27, by berghofe
Proofs are now hidden by default.
2005-01-27, by berghofe
- Proofs are now hidden by default
2005-01-27, by berghofe
Added show_var_qmarks flag.
2005-01-27, by berghofe
*** empty log message ***
2005-01-26, by nipkow
added OptionalSugar
2005-01-26, by nipkow
new
2005-01-26, by nipkow
moved to HOL/Library
2005-01-26, by nipkow
*** empty log message ***
2005-01-26, by nipkow
implemented cache for conversion to clauses
2005-01-26, by paulson
enclosed in (*<*) (*>*)
2005-01-25, by nipkow
Added variant of eres_inst_tac that operates on indexnames instead of strings.
2005-01-24, by berghofe
Adapted to modified interface of PureThy.get_thm(s).
2005-01-24, by berghofe
Eliminated hack for deleting leading question mark from induction
2005-01-24, by berghofe
Replaced xstring by thmref.
2005-01-24, by berghofe
Removed unnecessary subsignature checks to speed up rewriting.
2005-01-24, by berghofe
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
2005-01-24, by berghofe
Replaced xstring by thmref.
2005-01-24, by berghofe
Adapted to modified interface of PureThy.get_thm(s).
2005-01-24, by berghofe
Specific theorems in a named list of theorems can now be referred to
2005-01-24, by berghofe
updated description of arith_tac
2005-01-24, by paulson
thin_tac now works on P==>Q
2005-01-24, by paulson
some rationalizing of res_inst_tac
2005-01-24, by paulson
Jia Meng: delta simpsets and clasets
2005-01-21, by paulson
fixed thin_tac with higher-level assumptions by removing the old code to
2005-01-21, by paulson
inserted quotes preparatory to conversion
2005-01-21, by paulson
fixed the treatment of demodulation and paramodulation
2005-01-21, by paulson
negate_nead (???) changed to negated_asm_of_head
2005-01-21, by paulson
new theorem image_eq_fold
2005-01-21, by paulson
auto update
2005-01-21, by paulson
*** empty log message ***
2005-01-19, by nipkow
induct_tac and case_tac no longer depend on Syntax.string_of_vname.
2005-01-18, by berghofe
indexname function now parses type variables as well; changed input
2005-01-18, by berghofe
Added variants of instantiation functions that operate on pairs of type
2005-01-18, by berghofe
*** empty log message ***
2005-01-17, by nipkow
Removed div/mod ML code because it fails for 0.
2005-01-17, by nipkow
made diff_less a simp rule
2005-01-14, by nipkow
Added ChangeLog
2005-01-13, by berghofe
Tuned.
2005-01-11, by berghofe
Option for hiding proof scripts in documents.
2005-01-11, by berghofe
Added -H option for hiding proof scripts and other commands.
2005-01-11, by berghofe
Swapped session.ML and isar_output.ML
2005-01-11, by berghofe
Added flag for hiding proofs in documents to use_dir.
2005-01-11, by berghofe
Added table of commands to be hidden in LaTeX output.
2005-01-11, by berghofe
excursion_result now also passes previous state to presentation functions.
2005-01-11, by berghofe
Implemented hiding of proofs and other commands.
2005-01-11, by berghofe
new citation
2005-01-08, by nipkow
suggestions by Jeremy Siek
2005-01-06, by kleing
use ISO date format
2005-01-06, by kleing
added list_all_rev
2005-01-04, by kleing
[ .. (] -> [ ..< ]
2004-12-22, by nipkow
*** empty log message ***
2004-12-20, by nipkow
added simproc for Let
2004-12-18, by schirmer
added print translation for split: split f --> %(x,y). f x y
2004-12-18, by schirmer
Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
2004-12-18, by schirmer
Isabelle 2005 - preview
2004-12-17, by kleing
sugar, not sugari. stupid vi ;-)
2004-12-17, by kleing
removed two looping simplifications in SetInterval.thy; deleted the .ML file
2004-12-17, by paulson
*** empty log message ***
2004-12-17, by paulson
Further fix to a bug (involving equational premises) in inductive definitions
2004-12-16, by paulson
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
2004-12-16, by paulson
LaTeXsugar
2004-12-16, by kleing
removal of archaic Abs/Rep proofs
2004-12-15, by paulson
*** empty log message ***
2004-12-15, by paulson
removal of HOL_Lemmas
2004-12-15, by paulson
converted Relation_Power to new-style theory
2004-12-14, by paulson
new and stronger lemmas and improved simplification for finite sets
2004-12-14, by paulson
tidied; removed references to HOL theories
2004-12-14, by paulson
added find_rewrites
2004-12-13, by nipkow
*** empty log message ***
2004-12-13, by nipkow
added find_rewrites
2004-12-13, by nipkow
removal of NatArith.ML and Product_Type.ML
2004-12-13, by paulson
Fix pgmlsymbolson/off.
2004-12-13, by aspinall
REorganized Finite_Set
2004-12-12, by nipkow
Support PGIP <whitespace>, <dostep>, <doitem> elements as input
2004-12-10, by aspinall
Insert pgmltext element into responses in PGIP mode
2004-12-10, by aspinall
Added term cache to function condrew in order to speed up rewriting.
2004-12-10, by berghofe
- Exported functions new_name and new_names
2004-12-10, by berghofe
Fixed bug in mk_gen_of_def that could cause non-termination of the generator
2004-12-10, by berghofe
Preprocessors now transfer theorems to current theory in order to
2004-12-10, by berghofe
Moved code generator setup for product type to Product_Type.thy
2004-12-10, by berghofe
New code generator for let and split.
2004-12-10, by berghofe
Realizer for exE now uses let instead of case.
2004-12-10, by berghofe
First step in reorganizing Finite_Set
2004-12-09, by nipkow
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
2004-12-09, by paulson
Comments and other tweaks by Jia
2004-12-09, by paulson
*** empty log message ***
2004-12-09, by nipkow
converted Datatype_Universe to new-style theory
2004-12-09, by paulson
fixed bug in find functions that I introduced some time ago.
2004-12-08, by nipkow
converted Lfp to new-style theory
2004-12-08, by paulson
improvements by Larry and Micheal Wahler
2004-12-08, by kleing
renamed attributes to lower case
2004-12-07, by paulson
made proofs more robust
2004-12-07, by paulson
all theories must be related to Reconstruction
2004-12-07, by paulson
converted Gfp to new-style theory
2004-12-07, by paulson
proof of subst by S Merz
2004-12-07, by paulson
comment added
2004-12-07, by webertj
link to tar.gz
2004-12-07, by kleing
proof of subst by S Merz
2004-12-07, by paulson
Started to clean up and generalize FiniteSet
2004-12-06, by nipkow
add latex sugar
2004-12-06, by kleing
moved to Sugar
2004-12-06, by kleing
fixed typos
2004-12-06, by kleing
ignore generated
2004-12-06, by kleing
fixes to clause conversion
2004-12-03, by paulson
trying to fix the transfer problem
2004-12-03, by paulson
tidied
2004-12-03, by paulson
tuned
2004-12-03, by kleing
fixed typo
2004-12-03, by kleing
more sugar
2004-12-03, by kleing
clauses counted from 0
2004-12-02, by paulson
*** empty log message ***
2004-12-02, by nipkow
Fixed print translation for ALL x > y etc
2004-12-02, by nipkow
added ALL print-translation for > and >=.
2004-12-02, by nipkow
*** empty log message ***
2004-12-02, by nipkow
Added "ALL x > y" and relatives.
2004-12-02, by nipkow
new CLAUSIFY attribute for proof reconstruction with lemmas
2004-12-02, by paulson
*** empty log message ***
2004-12-02, by nipkow
antiquotations lhs and rhs
2004-12-02, by kleing
*** empty log message ***
2004-12-01, by nipkow
Removed postfix >= because of new >= sugar
2004-12-01, by nipkow
Added > and >= sugar
2004-12-01, by nipkow
>= became > = because of new >=
2004-12-01, by nipkow
fixed presentation
2004-12-01, by paulson
resolution package tools by Jia Meng
2004-12-01, by paulson
new antiquotations @{lhs thm} and @{rhs thm}
2004-12-01, by kleing
added antiquotations @{lhs thm} and @{rhs thm}
2004-12-01, by kleing
fixed another _
2004-12-01, by kleing
resolution package tools by Jia Meng
2004-11-30, by paulson
converted Wellfounded_Relations to Isar script
2004-11-30, by paulson
even more mboxes
2004-11-30, by schirmer
Rule: put \mbox around premises/conclusion to avoid problems with
2004-11-30, by schirmer
blast_tac -> blast in comment (fix latex error)
2004-11-30, by kleing
*** empty log message ***
2004-11-29, by nipkow
converted to Isar script, simplifying some results
2004-11-29, by paulson
obselete
2004-11-29, by nipkow
onsolete
2004-11-29, by nipkow
obsolete
2004-11-29, by nipkow
New
2004-11-29, by nipkow
render \<circ> as o not &circ; (which is ^)
2004-11-29, by kleing
minor code refactoring (typ_of_dtyp, size_of_dtyp)
2004-11-25, by webertj
exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
2004-11-25, by webertj
comments edited
2004-11-25, by webertj
added ZCHAFF_VERSION
2004-11-25, by webertj