Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-384
+384
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
replaced bool by a new datatype "bit" for binary numerals
2005-03-23, by paulson
temporary removal of Import
2005-03-23, by paulson
tidied
2005-03-23, by paulson
auto update
2005-03-22, by paulson
deleted a pointless comment
2005-03-22, by paulson
ensuring that "equal" is not a function
2005-03-22, by paulson
auto update
2005-03-18, by paulson
meson now checks that problems are first-order
2005-03-17, by paulson
added string_of_term
2005-03-17, by nipkow
Bugfix related to the interpretation of IDT constructors
2005-03-17, by webertj
more concise ASCII escaping
2005-03-15, by paulson
fixed syntax for Let <x,y> = a in e
2005-03-14, by huffman
bug fixes involving typechecking clauses
2005-03-14, by paulson
removed theorems about Sinl_Rep and Sinr_Rep
2005-03-12, by huffman
simplified some definitions, many proofs are much shorter
2005-03-11, by huffman
minor Library.option related modifications
2005-03-11, by webertj
code reformatted
2005-03-11, by webertj
code reformatted
2005-03-11, by webertj
fixed bug: domain package can now define three or more mutually recursive types simultaneously
2005-03-11, by huffman
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
2005-03-11, by huffman
fixed filename in header
2005-03-10, by huffman
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
2005-03-10, by huffman
Registrations of global locale interpretations: improved, better naming.
2005-03-10, by ballarin
Debugging code (error_depth) removed.
2005-03-10, by ballarin
First version of global registration command.
2005-03-09, by ballarin
fix integer overflow in numeral syntax for SML NJ.
2005-03-08, by obua
fixed variable name
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
removed Cprod3_lemma1 and Cprod3_lemma2
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
added subsection headings, cleaned up some proofs
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
added subsections and text for document generation
2005-03-07, by huffman
Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
2005-03-07, by huffman
HTML 4.01 Transitional conformity
2005-03-07, by webertj
refute_params: default value itself=1 added (for type classes)
2005-03-07, by webertj
HTML 4.01 Transitional conformity
2005-03-07, by webertj
HTML 4.01 Transitional conformity
2005-03-07, by webertj
now checks for higher-order vars
2005-03-07, by paulson
Cleaning up HOL/Matrix
2005-03-07, by obua
Tools/meson.ML: signature, structure and "open" rather than "local"
2005-03-07, by paulson
add header
2005-03-04, by huffman
fix headers
2005-03-04, by huffman
converted to new-style theories, and combined numbered files
2005-03-04, by huffman
document generation for HOLCF
2005-03-04, by huffman
Removed practically all references to Library.foldr.
2005-03-04, by skalberg
new first_order test
2005-03-04, by paulson
removed dead code
2005-03-04, by paulson
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 ˆ (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
added ZCHAFF_VERSION
2004-11-25, by webertj
ML
2004-11-25, by paulson
Removed a "Matches are not exhaustive" warning
2004-11-24, by webertj
mod because of change in finite set induction
2004-11-24, by nipkow
changed the order of !!-quantifiers in finite set induction.
2004-11-24, by nipkow
Made test_term escape special characters in strings that caused the
2004-11-24, by berghofe
Functions nat_to_bv and bv_to_nat now really operate on natural numbers.
2004-11-24, by berghofe
Added EfficientNat
2004-11-24, by berghofe
Code generator plug-in for implementing natural numbers by integers.
2004-11-24, by berghofe
Added Library/EfficientNat
2004-11-24, by berghofe
Reimplemented some operations on "code lemma" table to avoid that code
2004-11-24, by berghofe
New theorem zpower_int
2004-11-24, by berghofe
*** empty log message ***
2004-11-24, by nipkow
prettier proof of setsum_diff
2004-11-23, by obua
HTML conformity
2004-11-23, by webertj
renamed 1 lemmas
2004-11-23, by nipkow
renamed 2 lemmas
2004-11-23, by nipkow
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
2004-11-23, by obua
external solvers may now overwrite existing temporary files
2004-11-23, by webertj
added lemma
2004-11-23, by nipkow
Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
2004-11-23, by obua
*** empty log message ***
2004-11-23, by nipkow
generalized lemma
2004-11-23, by nipkow
added lemma
2004-11-23, by nipkow
indentation
2004-11-22, by paulson
fixed proof
2004-11-22, by nipkow
added lemmas
2004-11-22, by nipkow
Added more lemmas
2004-11-21, by nipkow
added lemmas
2004-11-21, by nipkow
Restructured List and added "rotate"
2004-11-21, by nipkow
comment modified
2004-11-19, by webertj
moved and renamed Integ/Equiv.thy
2004-11-19, by paulson
solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
2004-11-19, by webertj
Barith removed
2004-11-19, by chaieb
imports (new syntax for theory headers)
2004-11-18, by webertj
Tuned.
2004-11-18, by berghofe
replace strangely encode space characters by
2004-11-17, by kleing
replaced strangely encoded space characters by
2004-11-17, by kleing
removed explicit mentioning of zChaffs version number
2004-11-17, by webertj
minor changes (comments/code refactoring)
2004-11-17, by webertj
removed Exercises document (available on separate web site now)
2004-11-17, by kleing
removed exercised document
2004-11-17, by kleing
Markup obtain as introducing a nested goal.
2004-11-16, by aspinall
removed a "clone" (duplicate code)
2004-11-15, by paulson
minor rewording
2004-11-15, by webertj
Add <undoitem> for theory-state undos.
2004-11-15, by aspinall
Renamed some variables to eliminate conflicts with constants.
2004-11-15, by paulson
*** empty log message ***
2004-11-14, by webertj
DOCTYPE declaration added
2004-11-14, by webertj
Exercises added
2004-11-13, by webertj
More lemmas
2004-11-13, by nipkow
minor code refactoring
2004-11-12, by webertj
improved "subscribe" link
2004-11-12, by paulson
added DOCTYPE and Content-Type declarations to make this a valid HTML file
2004-11-12, by webertj
isatool usedir -f
2004-11-12, by webertj
updated subscription wording and link
2004-11-11, by paulson
increased tracing and search bounds
2004-11-11, by paulson
tidied comments
2004-11-08, by paulson
* extended interface of record_split_simp_tac and record_split_simproc
2004-11-05, by schirmer
user-interface impoved
2004-11-02, by chaieb
fixed some awkward problems with nat/int simprocs
2004-10-29, by paulson
fixed reference to renamed theorem
2004-10-29, by paulson
isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
2004-10-28, by webertj
Make <undostep> call undos_proof to display resulting proofstate.
2004-10-28, by aspinall
efficienty improvement
2004-10-28, by chaieb
Revert change to pgml_sym
2004-10-27, by aspinall
Added type constraint to make SML/NJ happy.
2004-10-27, by berghofe
Changed function cabs to also allow abstraction over Vars.
2004-10-26, by berghofe
Added function merge_alists'.
2004-10-26, by berghofe
Added function strip_type (for ctyps).
2004-10-26, by berghofe
Added preprocessors.
2004-10-26, by berghofe
Added setup for code generator.
2004-10-26, by berghofe
Added simple code generator.
2004-10-26, by berghofe
Removed code generator stuff. Code generation is now handled by code
2004-10-26, by berghofe
Added call to Codegen.preprocess.
2004-10-26, by berghofe
Fixed problem with sorts in function make_casedists.
2004-10-26, by berghofe
fixed urls
2004-10-25, by nipkow
Simplification to symbol processing; put quotes around theory name in message.
2004-10-24, by aspinall
Fix <closetheory>
2004-10-21, by aspinall
Replaced PolyML specific print function by Display.print_thm(s)
2004-10-19, by berghofe
converted some induct_tac to induct
2004-10-19, by paulson
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
2004-10-18, by dixon
Replaced list of bound variables in simpset by maximal index of bound
2004-10-18, by berghofe
record_split_simp_tac now can get simp rules as parameter
2004-10-15, by schirmer
update
2004-10-15, by nipkow
added and renamed
2004-10-15, by nipkow
Added a few lemmas
2004-10-14, by nipkow
mod becuase of chnage in induct
2004-10-13, by nipkow
Added solution to exercise.
2004-10-12, by nipkow
*** empty log message ***
2004-10-12, by nipkow
tweaks concerned with poly bug-fixing
2004-10-12, by paulson
Replaced the_context() by theory "Presburger" in call of invoke_oracle.
2004-10-11, by berghofe
Tuned some proofs.
2004-10-11, by berghofe
Added entry in Settings menu for Toplevel.skip_proofs flag.
2004-10-11, by berghofe
Some changes to allow skipping of proof scripts.
2004-10-11, by berghofe
less
more
|
(0)
-10000
-3000
-1000
-384
+384
+1000
+3000
+10000
+30000
tip