Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/HOL/Main.thy
2009-02-13
nipkow
2009-02-13
Moved Nat_Int_Bij into Library
file
|
diff
|
annotate
2009-02-06
blanchet
2009-02-06
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML + find/fix Product_Type.{fst,snd}, which are now called simply fst and snd.
file
|
diff
|
annotate
2009-01-02
wenzelm
2009-01-02
tuned header and description of boot files;
file
|
diff
|
annotate
2008-09-17
wenzelm
2008-09-17
moved global ML bindings to global place;
file
|
diff
|
annotate
2008-09-16
haftmann
2008-09-16
evaluation using code generator
file
|
diff
|
annotate
2008-09-02
nipkow
2008-09-02
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and distributed them over Real/ (to do with bijections and density). Library/NatPair became Nat_Int_Bij and made that part of Main.
file
|
diff
|
annotate
2008-06-26
haftmann
2008-06-26
added dummy citiation
file
|
diff
|
annotate
2008-04-22
haftmann
2008-04-22
dropped theory PreList
file
|
diff
|
annotate
2008-01-25
haftmann
2008-01-25
consistent interacitve bootstrap of HOL-Main
file
|
diff
|
annotate
2007-10-29
wenzelm
2007-10-29
qualified Proofterm.proofs;
file
|
diff
|
annotate
2007-09-27
paulson
2007-09-27
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
file
|
diff
|
annotate
2007-09-25
haftmann
2007-09-25
datatype interpretators for size and datatype_realizer
file
|
diff
|
annotate
2007-09-19
berghofe
2007-09-19
Enclosed end_theory in text antiquotation to make LaTeX happy.
file
|
diff
|
annotate
2007-09-18
paulson
2007-09-18
metis now available in PreList
file
|
diff
|
annotate
2007-05-31
wenzelm
2007-05-31
HOL_proofs;
file
|
diff
|
annotate
2007-05-06
haftmann
2007-05-06
minimal import
file
|
diff
|
annotate
2006-11-08
wenzelm
2006-11-08
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
file
|
diff
|
annotate
2006-08-25
paulson
2006-08-25
replaced skolem declarations by automatic skolemization of everything
file
|
diff
|
annotate
2006-08-08
paulson
2006-08-08
skolem declarations for built-in theorems
file
|
diff
|
annotate
2006-05-10
wenzelm
2006-05-10
revert accidental text change;
file
|
diff
|
annotate
2006-05-09
haftmann
2006-05-09
introduced characters for code generator; some improved code lemmas for some list functions
file
|
diff
|
annotate
2005-12-23
paulson
2005-12-23
the "skolem" attribute and better initialization of the clause database
file
|
diff
|
annotate
2005-12-01
paulson
2005-12-01
restoring the old status of subset_refl
file
|
diff
|
annotate
2005-10-19
mengj
2005-10-19
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
file
|
diff
|
annotate
2005-09-29
wenzelm
2005-09-29
explicit dependencies of SAT vs. Refute; moved late refute setup to SAT;
file
|
diff
|
annotate
2005-09-23
webertj
2005-09-23
new sat tactic imports resolution proofs from zChaff
file
|
diff
|
annotate
2005-09-23
webertj
2005-09-23
header (title/ID) added
file
|
diff
|
annotate
2005-09-23
webertj
2005-09-23
typo fixed: rufute -> refute
file
|
diff
|
annotate
2005-09-20
wenzelm
2005-09-20
removed Commutative_Ring hacks;
file
|
diff
|
annotate
2005-09-17
wenzelm
2005-09-17
minor cleanup, moved stuff in its proper place;
file
|
diff
|
annotate
2005-09-15
paulson
2005-09-15
moving Commutative_Ring to the correct theory
file
|
diff
|
annotate
2005-09-14
wenzelm
2005-09-14
hide the rather generic names used in theory Commutative_Ring;
file
|
diff
|
annotate
2005-09-14
wenzelm
2005-09-14
imports Commutative_Ring;
file
|
diff
|
annotate
2005-07-12
berghofe
2005-07-12
Auxiliary functions to be used in generated code are now defined using "attach".
file
|
diff
|
annotate
2005-07-01
berghofe
2005-07-01
Moved some code lemmas from Main to Nat.
file
|
diff
|
annotate
2005-06-28
paulson
2005-06-28
Constant "If" is now local
file
|
diff
|
annotate
2005-05-16
paulson
2005-05-16
Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
file
|
diff
|
annotate
2005-04-28
paulson
2005-04-28
fixed treatment of higher-order simprules
file
|
diff
|
annotate
2005-03-07
webertj
2005-03-07
refute_params: default value itself=1 added (for type classes)
file
|
diff
|
annotate
2005-02-13
skalberg
2005-02-13
Deleted Library.option type.
file
|
diff
|
annotate
2004-12-10
berghofe
2004-12-10
Moved code generator setup for product type to Product_Type.thy
file
|
diff
|
annotate
2004-12-07
paulson
2004-12-07
all theories must be related to Reconstruction
file
|
diff
|
annotate
2004-08-20
paulson
2004-08-20
proof reconstruction for external ATPs
file
|
diff
|
annotate
2004-08-18
nipkow
2004-08-18
import -> imports
file
|
diff
|
annotate
2004-08-16
nipkow
2004-08-16
New theory header syntax.
file
|
diff
|
annotate
2004-07-19
berghofe
2004-07-19
Moved code generator setup for lists to List.thy
file
|
diff
|
annotate
2004-06-21
kleing
2004-06-21
Merged in license change from Isabelle2004
file
|
diff
|
annotate
2004-05-26
webertj
2004-05-26
new default parameters for refute
file
|
diff
|
annotate
2004-03-26
webertj
2004-03-26
satsolver=dpll
file
|
diff
|
annotate
2004-03-10
webertj
2004-03-10
changed default values for refute
file
|
diff
|
annotate
2004-03-08
paulson
2004-03-08
generic theorems about exponentials; general tidying up
file
|
diff
|
annotate
2004-01-10
webertj
2004-01-10
Adding 'refute' to HOL.
file
|
diff
|
annotate
2003-09-22
berghofe
2003-09-22
Improved efficiency of code generated for < predicate on natural numbers.
file
|
diff
|
annotate
2003-07-11
berghofe
2003-07-11
- Installed specific code generator for equality enforcing that arguments do not have function types, which would result in an error message during compilation. - Added test case generators for basic types.
file
|
diff
|
annotate
2003-05-27
berghofe
2003-05-27
Added term_of function for product type.
file
|
diff
|
annotate
2002-12-16
berghofe
2002-12-16
Added mk_int and mk_list.
file
|
diff
|
annotate
2002-07-21
berghofe
2002-07-21
Added theory for setting up program extraction.
file
|
diff
|
annotate
2002-07-16
wenzelm
2002-07-16
moved stuff to List.thy;
file
|
diff
|
annotate
2002-04-19
berghofe
2002-04-19
code generator: wfrec combinator is now implemented by ML function wf_rec.
file
|
diff
|
annotate
2001-12-20
berghofe
2001-12-20
Declared characteristic equations for < on nat for code generation.
file
|
diff
|
annotate