Wed, 02 Jan 2008 15:14:15 +0100 |
haftmann |
improved evaluation mechanism
|
file |
diff |
annotate
|
Thu, 20 Dec 2007 14:33:40 +0100 |
wenzelm |
moved Pure/General/random_word.ML to Tools/random_word.ML;
|
file |
diff |
annotate
|
Thu, 20 Dec 2007 12:02:46 +0100 |
wenzelm |
updated HOL-Nominal-Examples deps;
|
file |
diff |
annotate
|
Tue, 11 Dec 2007 10:23:05 +0100 |
haftmann |
joined EvenOdd theory with Parity
|
file |
diff |
annotate
|
Fri, 07 Dec 2007 10:59:03 +0100 |
krauss |
Adding "ex/Induction_Scheme.thy" to tests
|
file |
diff |
annotate
|
Thu, 06 Dec 2007 15:10:09 +0100 |
haftmann |
added new primrec package
|
file |
diff |
annotate
|
Wed, 05 Dec 2007 14:16:15 +0100 |
haftmann |
dropped Classpackage.thy
|
file |
diff |
annotate
|
Tue, 13 Nov 2007 10:59:26 +0100 |
berghofe |
Added new program extraction examples.
|
file |
diff |
annotate
|
Tue, 06 Nov 2007 22:50:39 +0100 |
wenzelm |
activated HOL-SizeChange;
|
file |
diff |
annotate
|
Tue, 06 Nov 2007 20:27:33 +0100 |
wenzelm |
removed dependencies on Size_Change_Termination from HOL-Library;
|
file |
diff |
annotate
|
Tue, 06 Nov 2007 17:44:53 +0100 |
krauss |
moved stuff about size change termination to its own session
|
file |
diff |
annotate
|
Mon, 05 Nov 2007 22:50:48 +0100 |
kleing |
add root.bib for Word document
|
file |
diff |
annotate
|
Wed, 24 Oct 2007 19:21:39 +0200 |
wenzelm |
fixed HOL-Statespace for case-sensitive file-system;
|
file |
diff |
annotate
|
Wed, 24 Oct 2007 18:36:09 +0200 |
schirmer |
added Statespace library
|
file |
diff |
annotate
|
Fri, 12 Oct 2007 08:21:09 +0200 |
haftmann |
consolidated naming conventions for code generator theories
|
file |
diff |
annotate
|
Mon, 08 Oct 2007 22:03:25 +0200 |
haftmann |
integrated FixedPoint into Inductive
|
file |
diff |
annotate
|
Mon, 08 Oct 2007 07:09:29 +0200 |
urbanc |
changed VC-Compatible to VC_Compatible
|
file |
diff |
annotate
|
Mon, 08 Oct 2007 05:27:52 +0200 |
urbanc |
added the two new examples from Nominal to the build process
|
file |
diff |
annotate
|
Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
Sat, 29 Sep 2007 10:40:12 +0200 |
kleing |
Added target for proof term sessions (those that need -p 2)
|
file |
diff |
annotate
|
Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 18:05:34 +0200 |
wenzelm |
moved Tools/integer.ML to Pure/General/integer.ML;
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 07:46:00 +0200 |
haftmann |
introduced generic concepts for theory interpretators
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 07:36:38 +0200 |
haftmann |
separated code for inductive sequences from inductive_codegen.ML
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 06:21:40 +0200 |
nipkow |
sorting
|
file |
diff |
annotate
|
Sun, 16 Sep 2007 21:04:44 +0200 |
wenzelm |
added Induct/Common_Patterns.thy;
|
file |
diff |
annotate
|
Thu, 06 Sep 2007 11:52:13 +0200 |
berghofe |
- New theories Lambda/NormalForm and Lambda/Standardization
|
file |
diff |
annotate
|
Wed, 29 Aug 2007 13:58:00 +0200 |
wenzelm |
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
|
file |
diff |
annotate
|
Wed, 29 Aug 2007 11:10:28 +0200 |
wenzelm |
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 20:13:47 +0200 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 18:24:34 +0200 |
berghofe |
codegen.ML is now loaded in Pure again.
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 03:56:24 +0200 |
huffman |
HOL-Word-Examples
|
file |
diff |
annotate
|
Thu, 23 Aug 2007 16:47:16 +0200 |
huffman |
Word/BinInduct.thy
|
file |
diff |
annotate
|
Wed, 22 Aug 2007 21:09:21 +0200 |
huffman |
removed Word/Size.thy;
|
file |
diff |
annotate
|
Wed, 22 Aug 2007 16:54:43 +0200 |
huffman |
Word/WordBoolList.thy
|
file |
diff |
annotate
|
Tue, 21 Aug 2007 00:24:10 +0200 |
wenzelm |
use HOL-ex later;
|
file |
diff |
annotate
|
Mon, 20 Aug 2007 17:34:04 +0200 |
huffman |
Word/document/root.tex
|
file |
diff |
annotate
|
Mon, 20 Aug 2007 04:34:31 +0200 |
kleing |
* HOL-Word:
|
file |
diff |
annotate
|
Mon, 20 Aug 2007 00:22:18 +0200 |
kleing |
boolean algebras as locales and numbers as types by Brian Huffman
|
file |
diff |
annotate
|
Sat, 18 Aug 2007 17:42:38 +0200 |
wenzelm |
converted ex/MT.ML;
|
file |
diff |
annotate
|
Sat, 18 Aug 2007 13:32:28 +0200 |
wenzelm |
make HOL-ex earlier;
|
file |
diff |
annotate
|
Wed, 15 Aug 2007 15:06:58 +0200 |
paulson |
combining the relevance filter with res_atp
|
file |
diff |
annotate
|
Wed, 15 Aug 2007 08:57:39 +0200 |
haftmann |
updated code generator setup
|
file |
diff |
annotate
|
Thu, 09 Aug 2007 15:52:42 +0200 |
haftmann |
re-eliminated Option.thy
|
file |
diff |
annotate
|
Tue, 07 Aug 2007 09:38:44 +0200 |
haftmann |
split off theory Option for benefit of code generator
|
file |
diff |
annotate
|
Fri, 03 Aug 2007 22:35:40 +0200 |
wenzelm |
reactivated Nominal/Examples/Class.thy;
|
file |
diff |
annotate
|
Fri, 03 Aug 2007 16:28:18 +0200 |
wenzelm |
added dependency on Tools/Metis/metis.ML;
|
file |
diff |
annotate
|
Thu, 02 Aug 2007 15:44:37 +0200 |
wenzelm |
converted Meson tests to proper theory;
|
file |
diff |
annotate
|
Tue, 31 Jul 2007 22:21:18 +0200 |
wenzelm |
removed obsolete HOL/Real/ROOT.ML;
|
file |
diff |
annotate
|
Tue, 31 Jul 2007 19:40:22 +0200 |
wenzelm |
added Tools/lin_arith.ML;
|
file |
diff |
annotate
|
Tue, 31 Jul 2007 09:31:23 +0200 |
chaieb |
Added dependency on langford files in Tools/Qelim
|
file |
diff |
annotate
|
Sun, 29 Jul 2007 14:29:50 +0200 |
wenzelm |
removed obsolete Tools/res_atpset.ML;
|
file |
diff |
annotate
|
Fri, 20 Jul 2007 14:33:40 +0200 |
haftmann |
dropped Nat.ML legacy bindings
|
file |
diff |
annotate
|
Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 11:51:12 +0200 |
obua |
changed sources for HOL-Complex-Matrix
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 10:59:23 +0200 |
berghofe |
Added new package for inductive sets.
|
file |
diff |
annotate
|
Mon, 09 Jul 2007 22:06:49 +0200 |
wenzelm |
HOL-Complex-Matrix: fixed deps -- sort of;
|
file |
diff |
annotate
|
Thu, 05 Jul 2007 00:06:11 +0200 |
wenzelm |
added Tools/numeral.ML;
|
file |
diff |
annotate
|
Tue, 03 Jul 2007 18:00:57 +0200 |
chaieb |
Dependency on reflection_data.ML to build HOL-ex
|
file |
diff |
annotate
|
Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
file |
diff |
annotate
|
Tue, 26 Jun 2007 13:01:48 +0200 |
nipkow |
added NBE
|
file |
diff |
annotate
|
Mon, 25 Jun 2007 12:16:27 +0200 |
krauss |
removed "sum_tools.ML" in favour of BalancedTree
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 20:48:48 +0200 |
wenzelm |
moved quantifier elimination tools to Tools/Qelim/;
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 17:28:50 +0200 |
wenzelm |
renamed NatSimprocs.thy to Arith_Tools.thy;
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 15:42:07 +0200 |
wenzelm |
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 13:23:33 +0200 |
paulson |
integration of Metis prover
|
file |
diff |
annotate
|
Wed, 20 Jun 2007 23:19:17 +0200 |
wenzelm |
added Tools/metis_tools.ML;
|
file |
diff |
annotate
|
Mon, 11 Jun 2007 18:26:44 +0200 |
chaieb |
Added dependency on file Groebner_Basis.thy
|
file |
diff |
annotate
|
Mon, 11 Jun 2007 11:05:59 +0200 |
chaieb |
Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
|
file |
diff |
annotate
|
Wed, 06 Jun 2007 21:24:35 +0200 |
urbanc |
take out Class.thy again, because it does not yet compile cleanly
|
file |
diff |
annotate
|
Wed, 06 Jun 2007 16:12:08 +0200 |
chaieb |
New Reflected Presburger added to HOL/ex
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 22:46:55 +0200 |
wenzelm |
added ex/Groebner_Examples.thy;
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 20:46:25 +0200 |
chaieb |
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 16:26:04 +0200 |
wenzelm |
Semiring normalization and Groebner Bases.
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 15:16:08 +0200 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 09:56:19 +0200 |
urbanc |
included Class.thy in the compiling process for Nominal/Examples
|
file |
diff |
annotate
|
Sun, 03 Jun 2007 23:16:41 +0200 |
wenzelm |
HOL-ex: tuned deps;
|
file |
diff |
annotate
|
Fri, 01 Jun 2007 23:33:49 +0200 |
webertj |
tuned
|
file |
diff |
annotate
|
Fri, 01 Jun 2007 23:21:40 +0200 |
webertj |
some tests for arith added
|
file |
diff |
annotate
|
Fri, 01 Jun 2007 22:09:16 +0200 |
nipkow |
Moved list comprehension into List
|
file |
diff |
annotate
|
Thu, 31 May 2007 20:55:31 +0200 |
wenzelm |
moved IsaPlanner from Provers to Tools;
|
file |
diff |
annotate
|
Thu, 31 May 2007 18:16:52 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|
Thu, 31 May 2007 13:18:52 +0200 |
wenzelm |
moved TFL files to canonical place;
|
file |
diff |
annotate
|
Thu, 31 May 2007 12:06:31 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|
Thu, 31 May 2007 10:17:23 +0200 |
urbanc |
included new example in the compiling process
|
file |
diff |
annotate
|
Fri, 25 May 2007 18:08:34 +0200 |
nipkow |
Added List_Comprehension
|
file |
diff |
annotate
|
Fri, 25 May 2007 05:18:56 +0200 |
urbanc |
took out Class.thy from the compiling process until memory problems are solved
|
file |
diff |
annotate
|
Tue, 22 May 2007 05:07:48 +0200 |
huffman |
remove obsolete CSeries.thy
|
file |
diff |
annotate
|
Fri, 18 May 2007 09:16:57 +0200 |
haftmann |
dropped word_setup.ML
|
file |
diff |
annotate
|
Thu, 17 May 2007 23:03:47 +0200 |
krauss |
updated
|
file |
diff |
annotate
|
Tue, 15 May 2007 18:28:02 +0200 |
chaieb |
A verified theory for rational numbers representation and simple calculations;
|
file |
diff |
annotate
|
Mon, 14 May 2007 12:52:56 +0200 |
haftmann |
reorganized float arithmetic
|
file |
diff |
annotate
|
Sun, 13 May 2007 18:15:21 +0200 |
haftmann |
added modules rat.ML and int.ML
|
file |
diff |
annotate
|
Wed, 09 May 2007 19:37:22 +0200 |
wenzelm |
removed Complex/ComplexBin.thy;
|
file |
diff |
annotate
|
Sun, 06 May 2007 21:49:24 +0200 |
haftmann |
dropped HOL.ML
|
file |
diff |
annotate
|
Fri, 27 Apr 2007 14:21:23 +0200 |
urbanc |
alternative and much simpler proof for Church-Rosser of Beta-Reduction
|
file |
diff |
annotate
|
Thu, 26 Apr 2007 16:39:31 +0200 |
wenzelm |
removed legacy ML files;
|
file |
diff |
annotate
|
Thu, 26 Apr 2007 13:32:59 +0200 |
haftmann |
moved code generation pretty integers and characters to separate theories
|
file |
diff |
annotate
|
Tue, 24 Apr 2007 15:19:33 +0200 |
berghofe |
Added datatype_case.ML and nominal_fresh_fun.ML.
|
file |
diff |
annotate
|
Fri, 13 Apr 2007 10:00:04 +0200 |
ballarin |
New file for locale regression tests.
|
file |
diff |
annotate
|
Fri, 13 Apr 2007 00:07:52 +0200 |
huffman |
moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
|
file |
diff |
annotate
|
Thu, 12 Apr 2007 03:37:30 +0200 |
huffman |
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
|
file |
diff |
annotate
|
Wed, 11 Apr 2007 04:13:06 +0200 |
huffman |
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
|
file |
diff |
annotate
|
Tue, 27 Mar 2007 12:28:42 +0200 |
haftmann |
cleaned up HOL/ex/Code*.thy
|
file |
diff |
annotate
|
Mon, 26 Mar 2007 14:53:00 +0200 |
haftmann |
cleaned up Library( and ex/
|
file |
diff |
annotate
|
Fri, 23 Mar 2007 09:40:47 +0100 |
haftmann |
removed outdated example
|
file |
diff |
annotate
|
Tue, 20 Mar 2007 15:52:39 +0100 |
haftmann |
dropped OrderedGroup.ML
|
file |
diff |
annotate
|
Fri, 16 Mar 2007 21:33:31 +0100 |
haftmann |
dropped LOrder.thy
|
file |
diff |
annotate
|
Fri, 16 Mar 2007 17:17:36 +0100 |
urbanc |
adjusted for the example file SOS.thy
|
file |
diff |
annotate
|
Wed, 28 Feb 2007 16:35:00 +0100 |
krauss |
more cleanup
|
file |
diff |
annotate
|
Mon, 26 Feb 2007 21:34:16 +0100 |
krauss |
Added formalization of size-change principle (experimental).
|
file |
diff |
annotate
|
Fri, 16 Feb 2007 09:04:23 +0100 |
krauss |
updated Makefile
|
file |
diff |
annotate
|
Tue, 13 Feb 2007 18:19:25 +0100 |
berghofe |
Added new file Nominal/nominal_inductive.ML
|
file |
diff |
annotate
|
Wed, 07 Feb 2007 17:26:04 +0100 |
berghofe |
Added Predicate theory.
|
file |
diff |
annotate
|
Tue, 06 Feb 2007 00:53:15 +0100 |
urbanc |
corrected typo introduced by me
|
file |
diff |
annotate
|
Tue, 06 Feb 2007 00:41:54 +0100 |
urbanc |
moved the infrastructure from the nominal_tags file to nominal_thmdecls
|
file |
diff |
annotate
|
Mon, 22 Jan 2007 18:17:04 +0100 |
krauss |
Included ex/Fundefs.thy in HOL-ex session
|
file |
diff |
annotate
|
Mon, 22 Jan 2007 17:29:43 +0100 |
krauss |
* Preliminary implementation of tail recursion
|
file |
diff |
annotate
|
Sat, 20 Jan 2007 14:27:45 +0100 |
wenzelm |
added HOL/ex/Binary.thy;
|
file |
diff |
annotate
|
Fri, 19 Jan 2007 22:08:07 +0100 |
wenzelm |
HOL-Lambda: usedir -m no_brackets;
|
file |
diff |
annotate
|