| Tue, 06 Feb 2007 00:53:15 +0100 |
urbanc |
corrected typo introduced by me
|
changeset |
files
|
| Tue, 06 Feb 2007 00:43:23 +0100 |
urbanc |
now obsolete
|
changeset |
files
|
| Tue, 06 Feb 2007 00:41:54 +0100 |
urbanc |
moved the infrastructure from the nominal_tags file to nominal_thmdecls
|
changeset |
files
|
| Mon, 05 Feb 2007 15:55:32 +0100 |
krauss |
Exporting curried versions of tail recursive equations instead of internal ones
|
changeset |
files
|
| Mon, 05 Feb 2007 12:03:52 +0100 |
wenzelm |
proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:22 +0100 |
wenzelm |
removed non-modular comment;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:21 +0100 |
wenzelm |
interpretation: attempt to be more serious about name_morphism;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:20 +0100 |
wenzelm |
added full_naming;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:19 +0100 |
wenzelm |
tuned oracle interface;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:18 +0100 |
wenzelm |
added print_strings;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:17 +0100 |
wenzelm |
old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:16 +0100 |
wenzelm |
def_simproc(_i): tuned interface;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:15 +0100 |
wenzelm |
added cterm interface;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:14 +0100 |
wenzelm |
type simproc: explicitl dependency of morphism;
|
changeset |
files
|
| Sun, 04 Feb 2007 22:02:13 +0100 |
wenzelm |
load morphism.ML later;
|
changeset |
files
|
| Sat, 03 Feb 2007 23:42:55 +0100 |
urbanc |
added the two renaming functions from my PhD
|
changeset |
files
|
| Fri, 02 Feb 2007 17:16:16 +0100 |
urbanc |
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
|
changeset |
files
|
| Fri, 02 Feb 2007 15:47:58 +0100 |
nipkow |
a few additions and deletions
|
changeset |
files
|
| Thu, 01 Feb 2007 20:59:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Feb 2007 20:40:34 +0100 |
wenzelm |
proper use of PureThy.has_name_hint instead of hard-wired string'';
|
changeset |
files
|
| Thu, 01 Feb 2007 20:40:17 +0100 |
wenzelm |
removed non-modular comment;
|
changeset |
files
|
| Thu, 01 Feb 2007 13:41:19 +0100 |
paulson |
new theorem int_infinite
|
changeset |
files
|
| Wed, 31 Jan 2007 20:07:40 +0100 |
aspinall |
Fix tell_thm_deps to match changse in PureThy.
|
changeset |
files
|
| Wed, 31 Jan 2007 20:06:24 +0100 |
aspinall |
Expose hard-wired string which was changed and broke Proof General.
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:17 +0100 |
haftmann |
clarified error message
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:16 +0100 |
haftmann |
clarified command annotation
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:14 +0100 |
haftmann |
changed cong alist - now using AList operations instead of overwrite_warn
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:13 +0100 |
haftmann |
dropped Output.update_warn
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:12 +0100 |
haftmann |
print translation for record types with empty-sorted type variables raise Match instead of producing an error
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:10 +0100 |
haftmann |
dropped lemma duplicates in HOL.thy
|
changeset |
files
|
| Wed, 31 Jan 2007 14:03:31 +0100 |
paulson |
Tidying; more debugging information. New reference unwanted_types.
|
changeset |
files
|
| Tue, 30 Jan 2007 13:17:02 +0100 |
aspinall |
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
|
changeset |
files
|
| Tue, 30 Jan 2007 13:16:58 +0100 |
aspinall |
Add get_succs
|
changeset |
files
|
| Tue, 30 Jan 2007 13:14:41 +0100 |
aspinall |
Add operations on preference tables (remove, set_default).
|
changeset |
files
|
| Tue, 30 Jan 2007 08:21:23 +0100 |
haftmann |
adjusted to new codegen_funcgr interface
|
changeset |
files
|
| Tue, 30 Jan 2007 08:21:22 +0100 |
haftmann |
added interface for plugging in preprocessors
|
changeset |
files
|
| Tue, 30 Jan 2007 08:21:19 +0100 |
haftmann |
additional auxiliary here
|
changeset |
files
|
| Tue, 30 Jan 2007 08:21:18 +0100 |
haftmann |
whitespace tuning
|
changeset |
files
|
| Tue, 30 Jan 2007 08:21:17 +0100 |
haftmann |
dropped dead code
|
changeset |
files
|
| Tue, 30 Jan 2007 08:21:16 +0100 |
haftmann |
shifted import order
|
changeset |
files
|
| Tue, 30 Jan 2007 08:21:15 +0100 |
haftmann |
dropped whitespace
|
changeset |
files
|
| Tue, 30 Jan 2007 08:21:13 +0100 |
haftmann |
changed name of interpretation linorder to order
|
changeset |
files
|
| Mon, 29 Jan 2007 19:58:14 +0100 |
wenzelm |
proper simproc_setup;
|
changeset |
files
|
| Mon, 29 Jan 2007 19:58:14 +0100 |
wenzelm |
added get_simproc, @{simproc};
|
changeset |
files
|
| Sun, 28 Jan 2007 23:29:17 +0100 |
wenzelm |
added interface for target_naming;
|
changeset |
files
|
| Sun, 28 Jan 2007 23:29:16 +0100 |
wenzelm |
added simproc_setup;
|
changeset |
files
|
| Sun, 28 Jan 2007 23:29:15 +0100 |
wenzelm |
added def_simproc(_i) -- define named simprocs;
|
changeset |
files
|
| Sun, 28 Jan 2007 23:29:14 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Sun, 28 Jan 2007 11:52:52 +0100 |
chaieb |
Now deals with simples cases where the input equations contain type variables
|
changeset |
files
|
| Fri, 26 Jan 2007 13:59:06 +0100 |
haftmann |
refined algorithm
|
changeset |
files
|
| Fri, 26 Jan 2007 13:59:04 +0100 |
haftmann |
clarified code
|
changeset |
files
|
| Fri, 26 Jan 2007 13:59:03 +0100 |
haftmann |
exported interface for explicit error messages
|
changeset |
files
|
| Fri, 26 Jan 2007 13:59:02 +0100 |
haftmann |
added NestedEnvironment
|
changeset |
files
|
| Fri, 26 Jan 2007 10:48:09 +0100 |
paulson |
Improved debugging
|
changeset |
files
|
| Fri, 26 Jan 2007 10:46:22 +0100 |
paulson |
Streamlined and improved debugging messages
|
changeset |
files
|
| Fri, 26 Jan 2007 10:46:15 +0100 |
nipkow |
more fixes of arithmetic for min/max.
|
changeset |
files
|
| Fri, 26 Jan 2007 10:24:33 +0100 |
paulson |
min/max lemmas (actually unused!)
|
changeset |
files
|
| Fri, 26 Jan 2007 10:24:12 +0100 |
paulson |
simplification of Suc/numeral combinations with min, max
|
changeset |
files
|
| Fri, 26 Jan 2007 10:22:42 +0100 |
paulson |
Fixed long-standing, MAJOR bug in "lt"
|
changeset |
files
|
| Fri, 26 Jan 2007 09:24:35 +0100 |
haftmann |
adjusted manual to improved treatment of overloaded constants
|
changeset |
files
|
| Thu, 25 Jan 2007 16:57:57 +0100 |
nipkow |
Allows evaluation of min/max o numerals.
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:56 +0100 |
haftmann |
fixed bug for OCaml bigints
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:51 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:50 +0100 |
haftmann |
added explicit maintainance of coregular code theorems for overloaded constants
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:49 +0100 |
haftmann |
dropped useless stuff
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:48 +0100 |
haftmann |
clarified code
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:46 +0100 |
haftmann |
added explicit query function for arities to subalgebra projection
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:45 +0100 |
haftmann |
not importing NestedEnvironment
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:42 +0100 |
haftmann |
adjusted to changes in class package
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:37 +0100 |
haftmann |
made executable
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:36 +0100 |
haftmann |
improved
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:35 +0100 |
haftmann |
fxied bug for OCaml bigints
|
changeset |
files
|
| Thu, 25 Jan 2007 09:32:34 +0100 |
haftmann |
adjusted names
|
changeset |
files
|
| Wed, 24 Jan 2007 20:54:21 +0100 |
wenzelm |
tuned eta_contract;
|
changeset |
files
|
| Wed, 24 Jan 2007 20:54:20 +0100 |
wenzelm |
updated timing;
|
changeset |
files
|
| Wed, 24 Jan 2007 17:10:50 +0100 |
paulson |
some new lemmas
|
changeset |
files
|
| Wed, 24 Jan 2007 13:15:16 +0100 |
aspinall |
Let <loadfile> execute even while a file is open interactively.
|
changeset |
files
|
| Tue, 23 Jan 2007 20:29:03 +0100 |
krauss |
fixes smlnj-related problem, updated signature
|
changeset |
files
|
| Tue, 23 Jan 2007 15:54:22 +0100 |
dixon |
added a fold up and fold down as separate functions and fixed zipto to
|
changeset |
files
|
| Mon, 22 Jan 2007 19:00:29 +0100 |
nipkow |
simplified proofs
|
changeset |
files
|
| Mon, 22 Jan 2007 18:17:04 +0100 |
krauss |
Included ex/Fundefs.thy in HOL-ex session
|
changeset |
files
|
| Mon, 22 Jan 2007 17:29:43 +0100 |
krauss |
* Preliminary implementation of tail recursion
|
changeset |
files
|
| Mon, 22 Jan 2007 16:53:33 +0100 |
aspinall |
Add location_of_position. Needs work elsewhere.
|
changeset |
files
|
| Mon, 22 Jan 2007 16:52:26 +0100 |
aspinall |
Test askref
|
changeset |
files
|
| Mon, 22 Jan 2007 16:52:02 +0100 |
aspinall |
Expose currently open file
|
changeset |
files
|
| Mon, 22 Jan 2007 16:51:29 +0100 |
aspinall |
Sync location with pgip.rnc, fixing attribute names
|
changeset |
files
|
| Mon, 22 Jan 2007 15:37:08 +0100 |
aspinall |
Add askrefs, setrefs, error_with_pos
|
changeset |
files
|
| Mon, 22 Jan 2007 15:36:58 +0100 |
aspinall |
Comments
|
changeset |
files
|
| Mon, 22 Jan 2007 15:34:15 +0100 |
aspinall |
Comment
|
changeset |
files
|
| Mon, 22 Jan 2007 15:33:42 +0100 |
aspinall |
Add line_of, name_of destructors.
|
changeset |
files
|
| Mon, 22 Jan 2007 15:08:48 +0100 |
krauss |
Added lemma nat_size[simp]: "size (n::nat) = n"
|
changeset |
files
|
| Mon, 22 Jan 2007 00:40:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Jan 2007 19:09:38 +0100 |
wenzelm |
improved fact references: thmref;
|
changeset |
files
|
| Sun, 21 Jan 2007 19:09:37 +0100 |
wenzelm |
added atomic, print_int;
|
changeset |
files
|
| Sun, 21 Jan 2007 19:09:36 +0100 |
wenzelm |
tuned ML setup;
|
changeset |
files
|
| Sun, 21 Jan 2007 19:09:35 +0100 |
wenzelm |
* ML in Isar: improved error reporting;
|
changeset |
files
|
| Sun, 21 Jan 2007 17:13:30 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Jan 2007 16:46:40 +0100 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
changeset |
files
|
| Sun, 21 Jan 2007 16:46:06 +0100 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
changeset |
files
|
| Sun, 21 Jan 2007 16:43:47 +0100 |
wenzelm |
tuned comments
|
changeset |
files
|
| Sun, 21 Jan 2007 16:43:46 +0100 |
wenzelm |
simplified ML setup;
|
changeset |
files
|
| Sun, 21 Jan 2007 16:43:45 +0100 |
wenzelm |
use_text: added name argument;
|
changeset |
files
|
| Sun, 21 Jan 2007 16:43:44 +0100 |
wenzelm |
moved File.use to ML_Context.use;
|
changeset |
files
|
| Sun, 21 Jan 2007 16:43:42 +0100 |
wenzelm |
use_text: added name argument;
|
changeset |
files
|
| Sun, 21 Jan 2007 13:27:41 +0100 |
nipkow |
Added simproc list_neq (prompted by an application)
|
changeset |
files
|
| Sun, 21 Jan 2007 13:26:44 +0100 |
nipkow |
Added lists-as-multisets functions
|
changeset |
files
|
| Sat, 20 Jan 2007 14:27:46 +0100 |
wenzelm |
Simple and efficient binary numerals.
|
changeset |
files
|
| Sat, 20 Jan 2007 14:27:45 +0100 |
wenzelm |
added HOL/ex/Binary.thy;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:27 +0100 |
wenzelm |
tuned ML setup;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:23 +0100 |
wenzelm |
* ML within Isar: antiquotations;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:22 +0100 |
wenzelm |
added @{theory};
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:21 +0100 |
wenzelm |
added the_context_finished;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:20 +0100 |
wenzelm |
Toplevel.debug: coincide with Output.debugging;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:19 +0100 |
wenzelm |
ML tactic: proper context for compile and runtime;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:17 +0100 |
wenzelm |
added @{simpset};
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:16 +0100 |
wenzelm |
added is_finished_thy;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:14 +0100 |
wenzelm |
Output.debug: non-strict;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:12 +0100 |
wenzelm |
tuned ML setup;
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:11 +0100 |
wenzelm |
added @{clasimpset};
|
changeset |
files
|
| Sat, 20 Jan 2007 14:09:10 +0100 |
wenzelm |
added @{claset};
|
changeset |
files
|
| Fri, 19 Jan 2007 22:31:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:14:23 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:10:35 +0100 |
wenzelm |
renamed Isar/isar_output.ML to Thy/thy_output.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:32 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:31 +0100 |
wenzelm |
results: proper context;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:30 +0100 |
wenzelm |
tuned Scan.extend_lexicon;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:29 +0100 |
wenzelm |
renamed IsarOutput to ThyOutput;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:28 +0100 |
wenzelm |
moved parts to spec_parse.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:27 +0100 |
wenzelm |
removed obsolete Method;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:26 +0100 |
wenzelm |
renamed IsarOutput to ThyOutput;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:25 +0100 |
wenzelm |
added various ML setup functions (from sign.ML, pure_thy.ML);
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:24 +0100 |
wenzelm |
removed obsolete Attribute;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:23 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:22 +0100 |
wenzelm |
renamed Isar/isar_output.ML to Thy/thy_output.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:21 +0100 |
wenzelm |
tuned signature of extend_lexicon;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:20 +0100 |
wenzelm |
moved ML translation interfaces to isar_cmd.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:19 +0100 |
wenzelm |
moved thm/thms to ml_context.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:18 +0100 |
wenzelm |
moved inst from drule.ML to old_goals.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:16 +0100 |
wenzelm |
tuned order;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:15 +0100 |
wenzelm |
renamed Isar/term_style.ML to Thy/term_style.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:14 +0100 |
wenzelm |
renamed Isar/thy_header.ML to Thy/thy_header.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:13 +0100 |
wenzelm |
ML context and antiquotations (material from context.ML);
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:12 +0100 |
wenzelm |
Parsers for complex specifications (material from outer_parse.ML);
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:11 +0100 |
wenzelm |
renamed Isar/isar_output.ML to Thy/thy_output.ML;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:10 +0100 |
wenzelm |
moved parts of OuterParse to SpecParse;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:08 +0100 |
wenzelm |
moved parts of OuterParse to SpecParse;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:07 +0100 |
wenzelm |
HOL-Lambda: usedir -m no_brackets;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:06 +0100 |
wenzelm |
simplified ML setup;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:04 +0100 |
wenzelm |
renamed IsarOutput to ThyOutput;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:03 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:08:01 +0100 |
wenzelm |
renamed IsarOutput to ThyOutput;
|
changeset |
files
|
| Fri, 19 Jan 2007 22:04:22 +0100 |
webertj |
interpreter for Finite_Set.finite added
|
changeset |
files
|
| Fri, 19 Jan 2007 21:20:10 +0100 |
webertj |
reformatted to 80 chars/line
|
changeset |
files
|
| Fri, 19 Jan 2007 15:13:47 +0100 |
chaieb |
Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset.
|
changeset |
files
|
| Fri, 19 Jan 2007 13:16:37 +0100 |
wenzelm |
adapted ML context operations;
|
changeset |
files
|
| Fri, 19 Jan 2007 13:09:37 +0100 |
wenzelm |
added generic_theory_of;
|
changeset |
files
|
| Fri, 19 Jan 2007 13:09:36 +0100 |
wenzelm |
added 'declaration' command;
|
changeset |
files
|
| Fri, 19 Jan 2007 13:09:35 +0100 |
wenzelm |
added 'declaration' command;
|
changeset |
files
|
| Fri, 19 Jan 2007 13:09:33 +0100 |
wenzelm |
adapted ML context operations;
|
changeset |
files
|
| Fri, 19 Jan 2007 13:09:32 +0100 |
wenzelm |
ML context: full generic context, tuned signature;
|
changeset |
files
|
| Fri, 19 Jan 2007 13:09:31 +0100 |
wenzelm |
updated
|
changeset |
files
|
| Thu, 18 Jan 2007 11:16:49 +0100 |
aspinall |
Fix pgmlsymbolsoff
|
changeset |
files
|
| Wed, 17 Jan 2007 19:29:55 +0100 |
urbanc |
tuned a bit the proofs
|
changeset |
files
|
| Wed, 17 Jan 2007 11:39:32 +0100 |
dixon |
correctled left/right following of another context in zipto.
|
changeset |
files
|
| Wed, 17 Jan 2007 09:53:50 +0100 |
paulson |
induction rules for trancl/rtrancl expressed using subsets
|
changeset |
files
|
| Wed, 17 Jan 2007 09:52:54 +0100 |
paulson |
Deleted mk_fol_type, since the constructors can be used directly
|
changeset |
files
|
| Wed, 17 Jan 2007 09:52:06 +0100 |
paulson |
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
|
changeset |
files
|
| Tue, 16 Jan 2007 14:11:25 +0100 |
urbanc |
fixed typo introduced by me
|
changeset |
files
|
| Tue, 16 Jan 2007 14:10:27 +0100 |
haftmann |
changed dictionary representation to explicit classrel witnesses
|
changeset |
files
|
| Tue, 16 Jan 2007 14:10:26 +0100 |
haftmann |
reverted order of classrels
|
changeset |
files
|
| Tue, 16 Jan 2007 14:10:24 +0100 |
haftmann |
cleanup
|
changeset |
files
|
| Tue, 16 Jan 2007 13:59:08 +0100 |
urbanc |
formalisation of Crary's chapter on logical relations
|
changeset |
files
|
| Tue, 16 Jan 2007 10:25:38 +0100 |
urbanc |
added capabilities to handle mutual inductions
|
changeset |
files
|
| Tue, 16 Jan 2007 08:12:09 +0100 |
haftmann |
refined and added example for ExecutableRat
|
changeset |
files
|
| Tue, 16 Jan 2007 08:07:00 +0100 |
haftmann |
introduced binding concept
|
changeset |
files
|
| Tue, 16 Jan 2007 08:06:59 +0100 |
haftmann |
slight cleanup
|
changeset |
files
|
| Tue, 16 Jan 2007 08:06:57 +0100 |
haftmann |
renamed locale partial_order to order
|
changeset |
files
|
| Tue, 16 Jan 2007 08:06:55 +0100 |
haftmann |
refined and added example for ExecutableRat
|
changeset |
files
|
| Tue, 16 Jan 2007 08:06:52 +0100 |
haftmann |
updated keywords
|
changeset |
files
|
| Mon, 15 Jan 2007 10:15:55 +0100 |
krauss |
added sections on mutual induction and patterns
|
changeset |
files
|
| Sun, 14 Jan 2007 09:57:29 +0100 |
paulson |
optimized translation of HO problems
|
changeset |
files
|
| Fri, 12 Jan 2007 15:37:21 +0100 |
ballarin |
Reverted to structure representation with records.
|
changeset |
files
|
| Fri, 12 Jan 2007 09:58:31 +0100 |
haftmann |
more term inspection
|
changeset |
files
|
| Fri, 12 Jan 2007 09:58:30 +0100 |
haftmann |
introduced binding concept
|
changeset |
files
|
| Fri, 12 Jan 2007 09:58:29 +0100 |
haftmann |
adjusted manual
|
changeset |
files
|
| Thu, 11 Jan 2007 16:53:12 +0100 |
paulson |
well-founded relations for the integers
|
changeset |
files
|
| Thu, 11 Jan 2007 01:34:23 +0100 |
webertj |
updated to mention the automatic unfolding of constants
|
changeset |
files
|
| Wed, 10 Jan 2007 20:17:26 +0100 |
wenzelm |
removed NameSpace.split -- use qualifier/base instead;
|
changeset |
files
|
| Wed, 10 Jan 2007 20:16:52 +0100 |
wenzelm |
fixed exit: proper type check of state;
|
changeset |
files
|
| Wed, 10 Jan 2007 19:19:24 +0100 |
webertj |
tuned
|
changeset |
files
|
| Wed, 10 Jan 2007 19:18:29 +0100 |
webertj |
minor comment change
|
changeset |
files
|
| Wed, 10 Jan 2007 19:17:52 +0100 |
webertj |
no unfolding necessary anymore (refute does that automatically now)
|
changeset |
files
|
| Wed, 10 Jan 2007 09:28:24 +0100 |
haftmann |
improved case patterns
|
changeset |
files
|
| Wed, 10 Jan 2007 08:58:35 +0100 |
haftmann |
added undefined in cases
|
changeset |
files
|
| Tue, 09 Jan 2007 19:09:01 +0100 |
haftmann |
named preprocessorts
|
changeset |
files
|
| Tue, 09 Jan 2007 19:09:00 +0100 |
haftmann |
cleanup
|
changeset |
files
|
| Tue, 09 Jan 2007 19:08:59 +0100 |
haftmann |
activated new class code
|
changeset |
files
|
| Tue, 09 Jan 2007 19:08:58 +0100 |
haftmann |
handling for "undefined" in case expressions
|
changeset |
files
|
| Tue, 09 Jan 2007 19:08:56 +0100 |
haftmann |
named preprocessors
|
changeset |
files
|
| Tue, 09 Jan 2007 18:13:55 +0100 |
paulson |
The "of 1, simplified" stopped working some time ago, leaving these simprules
|
changeset |
files
|
| Tue, 09 Jan 2007 18:12:59 +0100 |
paulson |
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
|
changeset |
files
|
| Tue, 09 Jan 2007 15:49:39 +0100 |
paulson |
simplified the resoution proofs
|
changeset |
files
|
| Tue, 09 Jan 2007 12:12:00 +0100 |
aspinall |
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
|
changeset |
files
|
| Tue, 09 Jan 2007 12:09:49 +0100 |
aspinall |
Add info fatality for error messages.
|
changeset |
files
|
| Tue, 09 Jan 2007 12:09:21 +0100 |
aspinall |
Add informfileoutdated and completed flag. This makes the PGIP messages match the Broker states.
|
changeset |
files
|
| Tue, 09 Jan 2007 08:32:50 +0100 |
haftmann |
slight cleanups
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:54 +0100 |
haftmann |
improved names
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:52 +0100 |
haftmann |
proper node names
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:51 +0100 |
haftmann |
slight cleanup
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:50 +0100 |
haftmann |
improved variable name handling
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:49 +0100 |
haftmann |
moved variable environments here
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:48 +0100 |
haftmann |
moved a lot to codegen_func.ML
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:47 +0100 |
haftmann |
typo
|
changeset |
files
|
| Tue, 09 Jan 2007 08:31:46 +0100 |
haftmann |
added map_abs_vars
|
changeset |
files
|
| Mon, 08 Jan 2007 12:26:13 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 07 Jan 2007 16:21:22 +0100 |
webertj |
print functions for typs and terms added
|
changeset |
files
|
| Sun, 07 Jan 2007 14:05:44 +0100 |
aspinall |
Be more chatty in PGIP file operations.
|
changeset |
files
|
| Sat, 06 Jan 2007 20:56:44 +0100 |
chaieb |
A few lemmas about relative primes when dividing trough gcd
|
changeset |
files
|
| Sat, 06 Jan 2007 20:47:09 +0100 |
chaieb |
A few theorems on integer divisibily.
|
changeset |
files
|
| Fri, 05 Jan 2007 17:38:05 +0100 |
paulson |
Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever
|
changeset |
files
|
| Fri, 05 Jan 2007 15:33:05 +0100 |
webertj |
reverted to v1.60 (PolyML 4.1.3 still has the wrong signature for Array.modifyi)
|
changeset |
files
|
| Fri, 05 Jan 2007 14:32:07 +0100 |
haftmann |
added codegen_func.ML
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:51 +0100 |
haftmann |
non-layout-sensitive syntax for Haskell
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:50 +0100 |
haftmann |
some cleanup
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:49 +0100 |
haftmann |
primitive definitions are always eta-expanded
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:48 +0100 |
haftmann |
added block_enclose
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:47 +0100 |
haftmann |
added CodeEval
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:46 +0100 |
haftmann |
dealing with ml_string and char instances
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:45 +0100 |
haftmann |
dealing with ml_string combinators
|
changeset |
files
|
| Fri, 05 Jan 2007 14:31:44 +0100 |
haftmann |
adaptions
|
changeset |
files
|
| Fri, 05 Jan 2007 14:30:08 +0100 |
wenzelm |
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
|
changeset |
files
|
| Fri, 05 Jan 2007 14:30:07 +0100 |
wenzelm |
RAW-ProofGeneral: more dependencies;
|
changeset |
files
|
| Fri, 05 Jan 2007 13:36:32 +0100 |
paulson |
Proof.context now sent to watcher and used in type inference step of proof reconstruction
|
changeset |
files
|
| Thu, 04 Jan 2007 21:58:46 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Thu, 04 Jan 2007 21:37:02 +0100 |
wenzelm |
removed obsolete ProofGeneral/syntax_standalone.ML;
|
changeset |
files
|
| Thu, 04 Jan 2007 21:36:52 +0100 |
wenzelm |
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
|
changeset |
files
|
| Thu, 04 Jan 2007 21:18:05 +0100 |
wenzelm |
added mk_simproc': tuned interface;
|
changeset |
files
|
| Thu, 04 Jan 2007 20:01:02 +0100 |
haftmann |
clarification
|
changeset |
files
|
| Thu, 04 Jan 2007 20:01:01 +0100 |
haftmann |
dropped function theorems are considered as deleted
|
changeset |
files
|
| Thu, 04 Jan 2007 20:01:00 +0100 |
haftmann |
examples for evaluation oracle
|
changeset |
files
|
| Thu, 04 Jan 2007 20:00:59 +0100 |
haftmann |
fixed eval oracle
|
changeset |
files
|
| Thu, 04 Jan 2007 19:53:00 +0100 |
aspinall |
Be more chatty in PGIP file operations.proof_general_pgip.ML
|
changeset |
files
|
| Thu, 04 Jan 2007 19:27:08 +0100 |
wenzelm |
broken error handling for command syntax -- reverted to revision 1.9;
|
changeset |
files
|
| Thu, 04 Jan 2007 18:09:58 +0100 |
aspinall |
Use warning fatality
|
changeset |
files
|
| Thu, 04 Jan 2007 18:09:30 +0100 |
aspinall |
Add warning fatality
|
changeset |
files
|
| Thu, 04 Jan 2007 17:55:12 +0100 |
paulson |
improvements to proof reconstruction. Some files loaded in a different order
|
changeset |
files
|
| Thu, 04 Jan 2007 17:52:28 +0100 |
webertj |
using Array.modifyi (no functional change)
|
changeset |
files
|
| Thu, 04 Jan 2007 17:49:43 +0100 |
wenzelm |
run as RAW session;
|
changeset |
files
|
| Thu, 04 Jan 2007 17:49:42 +0100 |
wenzelm |
removed obsolete option -C;
|
changeset |
files
|
| Thu, 04 Jan 2007 17:49:41 +0100 |
wenzelm |
removed obsolete Pure-copied target;
|
changeset |
files
|
| Thu, 04 Jan 2007 17:17:48 +0100 |
haftmann |
updated manual
|
changeset |
files
|
| Thu, 04 Jan 2007 17:11:09 +0100 |
haftmann |
updated manual
|
changeset |
files
|
| Thu, 04 Jan 2007 15:29:44 +0100 |
webertj |
obsolete sign_of calls removed
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:41 +0100 |
haftmann |
fixed output
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:40 +0100 |
haftmann |
different handling of eta expansion
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:39 +0100 |
haftmann |
eta-expansion now only to common maximum number of arguments
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:38 +0100 |
haftmann |
clarified code
|
changeset |
files
|
| Thu, 04 Jan 2007 14:01:37 +0100 |
haftmann |
more term examples
|
changeset |
files
|
| Thu, 04 Jan 2007 11:56:53 +0100 |
haftmann |
eliminated Option.app
|
changeset |
files
|
| Thu, 04 Jan 2007 00:12:30 +0100 |
webertj |
constants are unfolded, universal quantifiers are stripped, some minor changes
|
changeset |
files
|
| Wed, 03 Jan 2007 22:59:30 +0100 |
aspinall |
Fix error reporting in Emacs to also match Isar command failure exactly.
|
changeset |
files
|
| Wed, 03 Jan 2007 21:11:42 +0100 |
aspinall |
Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
|
changeset |
files
|
| Wed, 03 Jan 2007 21:09:13 +0100 |
aspinall |
Expose command failure recovery code for top level.
|
changeset |
files
|
| Wed, 03 Jan 2007 21:00:24 +0100 |
aspinall |
Selected functions from syntax module
|
changeset |
files
|
| Wed, 03 Jan 2007 18:30:57 +0100 |
paulson |
x-symbol is no longer switched off in the ATP linkup
|
changeset |
files
|
| Wed, 03 Jan 2007 18:29:46 +0100 |
paulson |
Improvements to proof reconstruction. Now "fixes" is inserted
|
changeset |
files
|
| Wed, 03 Jan 2007 11:06:52 +0100 |
paulson |
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
|
changeset |
files
|
| Wed, 03 Jan 2007 10:59:06 +0100 |
paulson |
first version of structured proof reconstruction
|
changeset |
files
|
| Tue, 02 Jan 2007 22:43:05 +0100 |
wenzelm |
Morphism.fact;
|
changeset |
files
|
| Tue, 02 Jan 2007 22:43:04 +0100 |
wenzelm |
Term.lambda: abstract over arbitrary closed terms;
|
changeset |
files
|
| Sun, 31 Dec 2006 15:57:58 +0100 |
aspinall |
Add standalone file to help porters
|
changeset |
files
|
| Sun, 31 Dec 2006 15:34:21 +0100 |
aspinall |
Quote arguments in PGIP exceptions. Tune comment.
|
changeset |
files
|
| Sun, 31 Dec 2006 14:55:35 +0100 |
aspinall |
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
|
changeset |
files
|
| Sun, 31 Dec 2006 14:50:40 +0100 |
aspinall |
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
|
changeset |
files
|
| Sat, 30 Dec 2006 16:20:32 +0100 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:10 +0100 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:09 +0100 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:07 +0100 |
wenzelm |
refrain from setting ml_prompts again;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:06 +0100 |
wenzelm |
removed misleading OuterLex.eq_token;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:05 +0100 |
wenzelm |
pretty_statement: more careful handling of name_hint;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:04 +0100 |
wenzelm |
added has_name_hint;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:03 +0100 |
wenzelm |
removed obsolete name_hint handling;
|
changeset |
files
|
| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:41:59 +0100 |
wenzelm |
removed obsolete support for polyml-4.9.1;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:38:51 +0100 |
wenzelm |
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:29 +0100 |
wenzelm |
inform_file_processed: Toplevel.init_empty;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:28 +0100 |
wenzelm |
refined notion of empty toplevel, admits undo of 'end';
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:27 +0100 |
wenzelm |
Toplevel.init_state;
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:26 +0100 |
wenzelm |
removed obsolete 'clear_undos';
|
changeset |
files
|
| Sat, 30 Dec 2006 12:33:25 +0100 |
wenzelm |
removed obsolete clear_undos_theory;
|
changeset |
files
|
| Fri, 29 Dec 2006 20:35:03 +0100 |
haftmann |
major restructurings
|
changeset |
files
|
| Fri, 29 Dec 2006 20:35:02 +0100 |
haftmann |
cleanup
|
changeset |
files
|
| Fri, 29 Dec 2006 20:34:18 +0100 |
haftmann |
improved print of constructors in OCaml
|
changeset |
files
|
| Fri, 29 Dec 2006 20:34:17 +0100 |
haftmann |
changed syntax for axclass attach
|
changeset |
files
|
| Fri, 29 Dec 2006 19:50:52 +0100 |
wenzelm |
removed obsolete cond_add_path;
|
changeset |
files
|
| Fri, 29 Dec 2006 19:50:51 +0100 |
wenzelm |
removed obsolete context_thy etc.;
|
changeset |
files
|
| Fri, 29 Dec 2006 19:50:50 +0100 |
wenzelm |
removed obsolete init_pgip;
|
changeset |
files
|
| Fri, 29 Dec 2006 19:50:48 +0100 |
wenzelm |
removed obsolete init_context;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:47:11 +0100 |
wenzelm |
obsolete (cf. ProofGeneral/proof_general_emacs.ML);
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:06 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:04 +0100 |
wenzelm |
signed_string_of_int;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:04 +0100 |
wenzelm |
added proper header;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:02 +0100 |
wenzelm |
added signed_string_of_int (pruduces proper - instead of SML's ~);
|
changeset |
files
|
| Fri, 29 Dec 2006 18:46:01 +0100 |
wenzelm |
removed obsolete proof_general.ML;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:25:46 +0100 |
wenzelm |
minor tuning;
|
changeset |
files
|
| Fri, 29 Dec 2006 18:25:45 +0100 |
wenzelm |
tuned specifications/proofs;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:49 +0100 |
wenzelm |
replaced Sign.classes by Sign.all_classes (topologically sorted);
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:49 +0100 |
wenzelm |
renamed Graph.project to Graph.subgraph;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:47 +0100 |
wenzelm |
replaced Sign.classes by Sign.all_classes (topologically sorted);
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:46 +0100 |
wenzelm |
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:45 +0100 |
wenzelm |
Sorts.minimal_classes;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:44 +0100 |
wenzelm |
classes: more direct way to achieve topological sorting;
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:43 +0100 |
wenzelm |
replaced classes by all_classes (topologically sorted);
|
changeset |
files
|
| Fri, 29 Dec 2006 17:24:41 +0100 |
wenzelm |
replaced Sign.classes by Sign.all_classes (topologically sorted);
|
changeset |
files
|
| Fri, 29 Dec 2006 16:47:49 +0100 |
aspinall |
Enable new Proof General code again after SML/NJ compatibility fixes by Florian.
|
changeset |
files
|
| Fri, 29 Dec 2006 16:46:39 +0100 |
aspinall |
Typo in last commit
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:05 +0100 |
haftmann |
explicit construction of operational classes
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:04 +0100 |
haftmann |
added handling for explicit classrel witnesses
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:03 +0100 |
haftmann |
``classes`` now returns classes in topological order
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:02 +0100 |
haftmann |
dropped some bookkeeping
|
changeset |
files
|
| Fri, 29 Dec 2006 12:11:00 +0100 |
haftmann |
simplified class_package
|
changeset |
files
|
| Fri, 29 Dec 2006 03:57:01 +0100 |
wenzelm |
use_ml: reverted to simple output (Poly/ML changed);
|
changeset |
files
|
| Thu, 28 Dec 2006 16:49:35 +0100 |
haftmann |
removed private files
|
changeset |
files
|
| Thu, 28 Dec 2006 14:30:41 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 28 Dec 2006 14:30:40 +0100 |
wenzelm |
removed nospaces (Char.isSpace does not conform to Isabelle conventions);
|
changeset |
files
|
| Thu, 28 Dec 2006 14:30:39 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Thu, 28 Dec 2006 14:30:38 +0100 |
wenzelm |
inlined nospaces (from library.ML);
|
changeset |
files
|
| Thu, 28 Dec 2006 10:04:10 +0100 |
haftmann |
added
|
changeset |
files
|
| Wed, 27 Dec 2006 19:10:07 +0100 |
haftmann |
some clarifications
|
changeset |
files
|
| Wed, 27 Dec 2006 19:10:06 +0100 |
haftmann |
different handling of type variable names
|
changeset |
files
|
| Wed, 27 Dec 2006 19:10:05 +0100 |
haftmann |
added split
|
changeset |
files
|
| Wed, 27 Dec 2006 19:10:04 +0100 |
haftmann |
fixed misleading error message
|
changeset |
files
|
| Wed, 27 Dec 2006 19:10:03 +0100 |
haftmann |
dropped section header
|
changeset |
files
|
| Wed, 27 Dec 2006 19:10:00 +0100 |
haftmann |
added OCaml code generation (without dictionaries)
|
changeset |
files
|
| Wed, 27 Dec 2006 19:09:59 +0100 |
haftmann |
removed Haskell reserved words
|
changeset |
files
|
| Wed, 27 Dec 2006 19:09:58 +0100 |
haftmann |
removed Main.thy
|
changeset |
files
|
| Wed, 27 Dec 2006 19:09:57 +0100 |
haftmann |
moved code generator product setup here
|
changeset |
files
|
| Wed, 27 Dec 2006 19:09:56 +0100 |
haftmann |
added code generator test theory
|
changeset |
files
|
| Wed, 27 Dec 2006 19:09:55 +0100 |
haftmann |
explizit serialization for Haskell id
|
changeset |
files
|
| Wed, 27 Dec 2006 19:09:54 +0100 |
haftmann |
removed code generation stuff belonging to other theories
|
changeset |
files
|
| Wed, 27 Dec 2006 19:09:53 +0100 |
haftmann |
moved code generator bool setup here
|
changeset |
files
|
| Wed, 27 Dec 2006 16:24:31 +0100 |
haftmann |
exported explicit equality on tokens
|
changeset |
files
|
| Wed, 27 Dec 2006 16:18:07 +0100 |
haftmann |
made SML/NJ happy
|
changeset |
files
|
| Fri, 22 Dec 2006 21:00:55 +0100 |
paulson |
revised for new make_clauses
|
changeset |
files
|
| Fri, 22 Dec 2006 21:00:42 +0100 |
paulson |
tidying the ATP communications
|
changeset |
files
|
| Fri, 22 Dec 2006 20:58:14 +0100 |
paulson |
string primtives
|
changeset |
files
|
| Fri, 22 Dec 2006 15:35:17 +0100 |
haftmann |
deactivated test for the moment
|
changeset |
files
|
| Fri, 22 Dec 2006 14:24:04 +0100 |
paulson |
fixed typo in comment
|
changeset |
files
|
| Fri, 22 Dec 2006 14:03:30 +0100 |
ballarin |
Experimenting with interpretations of "definition".
|
changeset |
files
|
| Thu, 21 Dec 2006 13:55:15 +0100 |
haftmann |
clarified code
|
changeset |
files
|
| Thu, 21 Dec 2006 13:55:14 +0100 |
haftmann |
dropped superfluos code
|
changeset |
files
|
| Thu, 21 Dec 2006 13:55:13 +0100 |
haftmann |
code clarifications
|
changeset |
files
|
| Thu, 21 Dec 2006 13:55:12 +0100 |
haftmann |
import path made absolute
|
changeset |
files
|
| Thu, 21 Dec 2006 13:55:11 +0100 |
haftmann |
added code lemmas for quantification over bounded nats
|
changeset |
files
|
| Thu, 21 Dec 2006 08:42:53 +0100 |
aspinall |
Disable new Proof General code until SML/NJ compile fixed.
|
changeset |
files
|
| Wed, 20 Dec 2006 18:38:27 +0100 |
aspinall |
Use new Proof General code by default [see comment for reverting]
|
changeset |
files
|
| Wed, 20 Dec 2006 17:03:46 +0100 |
paulson |
change from "Array" to "Vector"
|
changeset |
files
|
| Tue, 19 Dec 2006 19:34:35 +0100 |
huffman |
add lemmas Standard_starfun(2)_iff
|
changeset |
files
|
| Tue, 19 Dec 2006 17:35:33 +0100 |
aspinall |
Missing elements from doc_markup_elements
|
changeset |
files
|
| Tue, 19 Dec 2006 16:58:30 +0100 |
aspinall |
Remove obsolete prefixes from error and warning messages.
|
changeset |
files
|
| Mon, 18 Dec 2006 08:57:41 +0100 |
haftmann |
added isatool codegen
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:40 +0100 |
haftmann |
dropped CodegenPackage.const_of_idf
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:39 +0100 |
haftmann |
improvements in syntax handling
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:38 +0100 |
haftmann |
added Thyname.* and * constant expressions
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:37 +0100 |
haftmann |
introduces "__" naming policy
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:35 +0100 |
haftmann |
switched argument order in *.syntax lifters
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:34 +0100 |
haftmann |
added gen_reflection_tac
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:33 +0100 |
haftmann |
now testing executable content of nearly all HOL
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:32 +0100 |
haftmann |
dropped debug cmd
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:31 +0100 |
haftmann |
explicit nonfix declaration for ML "subset"
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:30 +0100 |
haftmann |
dropped two inline directives
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:29 +0100 |
haftmann |
introduced abstract view on number expressions in hologic.ML
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:28 +0100 |
haftmann |
whitespace fix
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:27 +0100 |
haftmann |
added code generation syntax for some char combinators
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:26 +0100 |
haftmann |
infix syntax for generated code for composition
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:25 +0100 |
haftmann |
new-style oracle setup
|
changeset |
files
|
| Mon, 18 Dec 2006 08:21:24 +0100 |
haftmann |
added functions tutorial
|
changeset |
files
|
| Sun, 17 Dec 2006 22:43:50 +0100 |
aspinall |
Add abstraction for objtypes and documents.
|
changeset |
files
|
| Sat, 16 Dec 2006 20:27:56 +0100 |
huffman |
removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy
|
changeset |
files
|
| Sat, 16 Dec 2006 20:23:45 +0100 |
huffman |
moved several theorems; rearranged theory dependencies
|
changeset |
files
|
| Sat, 16 Dec 2006 19:37:07 +0100 |
huffman |
hypreal_of_hypnat abbreviates more general of_hypnat
|
changeset |
files
|
| Fri, 15 Dec 2006 17:51:07 +0100 |
webertj |
tracing instead of warning
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:50 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:16 +0100 |
wenzelm |
removed obsolete assert;
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:15 +0100 |
wenzelm |
renamed LocalTheory.assert to affirm;
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:14 +0100 |
wenzelm |
tuned -- accomodate Alice;
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
changeset |
files
|
| Thu, 14 Dec 2006 22:19:39 +0100 |
huffman |
remove Hyperreal/fuf.ML
|
changeset |
files
|
| Thu, 14 Dec 2006 22:18:08 +0100 |
huffman |
remove commented section
|
changeset |
files
|
| Thu, 14 Dec 2006 22:09:26 +0100 |
huffman |
remove ultra tactic and redundant FreeUltrafilterNat lemmas
|
changeset |
files
|
| Thu, 14 Dec 2006 22:08:35 +0100 |
huffman |
declare insert_iff [simp]
|
changeset |
files
|
| Thu, 14 Dec 2006 21:46:59 +0100 |
wenzelm |
activated improved use_ml, which captures output and reports source positions;
|
changeset |
files
|
| Thu, 14 Dec 2006 21:46:58 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 14 Dec 2006 21:33:47 +0100 |
huffman |
prove hyperpow_realpow using transfer
|
changeset |
files
|
| Thu, 14 Dec 2006 21:03:39 +0100 |
huffman |
remove usage of ultra tactic
|
changeset |
files
|
| Thu, 14 Dec 2006 19:29:48 +0100 |
huffman |
add lemmas singleton and insert_iff
|
changeset |
files
|
| Thu, 14 Dec 2006 19:15:16 +0100 |
huffman |
generalized type of hyperpow; removed hcpow
|
changeset |
files
|
| Thu, 14 Dec 2006 18:10:38 +0100 |
huffman |
redefine hSuc as *f* Suc, and move to HyperNat.thy
|
changeset |
files
|
| Thu, 14 Dec 2006 16:08:09 +0100 |
wenzelm |
proper use of IntInf instead of InfInf;
|
changeset |
files
|
| Thu, 14 Dec 2006 15:31:22 +0100 |
wenzelm |
defs/notes: more robust transitivity reasoning;
|
changeset |
files
|
| Thu, 14 Dec 2006 15:31:21 +0100 |
wenzelm |
added trans_terms/props;
|
changeset |
files
|
| Thu, 14 Dec 2006 15:31:20 +0100 |
wenzelm |
locale: print context for begin;
|
changeset |
files
|
| Thu, 14 Dec 2006 01:19:27 +0100 |
huffman |
remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq
|
changeset |
files
|
| Wed, 13 Dec 2006 23:15:39 +0100 |
huffman |
remove uses of star_n and FreeUltrafilterNat
|
changeset |
files
|
| Wed, 13 Dec 2006 21:46:34 +0100 |
huffman |
remove use of FreeUltrafilterNat
|
changeset |
files
|
| Wed, 13 Dec 2006 21:25:56 +0100 |
huffman |
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
|
changeset |
files
|
| Wed, 13 Dec 2006 20:38:24 +0100 |
haftmann |
fixed type
|
changeset |
files
|
| Wed, 13 Dec 2006 20:38:23 +0100 |
haftmann |
added stub for OCaml serializer
|
changeset |
files
|
| Wed, 13 Dec 2006 20:38:20 +0100 |
haftmann |
cleanup
|
changeset |
files
|
| Wed, 13 Dec 2006 20:38:19 +0100 |
haftmann |
whitespace correction
|
changeset |
files
|
| Wed, 13 Dec 2006 20:38:18 +0100 |
haftmann |
clarifed comment
|
changeset |
files
|
| Wed, 13 Dec 2006 20:38:17 +0100 |
haftmann |
dropped FIXME comment
|
changeset |
files
|
| Wed, 13 Dec 2006 20:38:16 +0100 |
haftmann |
clarified character setup
|
changeset |
files
|
| Wed, 13 Dec 2006 19:39:48 +0100 |
huffman |
remove references to star_n
|
changeset |
files
|
| Wed, 13 Dec 2006 19:05:45 +0100 |
huffman |
SComplex abbreviates Standard
|
changeset |
files
|
| Wed, 13 Dec 2006 16:33:11 +0100 |
wenzelm |
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
|
changeset |
files
|
| Wed, 13 Dec 2006 16:32:20 +0100 |
wenzelm |
removed legacy ML bindings;
|
changeset |
files
|
| Wed, 13 Dec 2006 16:26:45 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 13 Dec 2006 15:47:37 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 13 Dec 2006 15:47:36 +0100 |
wenzelm |
internal_abbrev: observe print mode;
|
changeset |
files
|
| Wed, 13 Dec 2006 15:47:34 +0100 |
wenzelm |
target_abbrev: internal mode for abbrevs;
|
changeset |
files
|
| Wed, 13 Dec 2006 15:47:33 +0100 |
wenzelm |
edge: actually apply operation!
|
changeset |
files
|
| Wed, 13 Dec 2006 15:47:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 13 Dec 2006 15:45:33 +0100 |
haftmann |
authentic syntax for number_of
|
changeset |
files
|
| Wed, 13 Dec 2006 15:45:31 +0100 |
haftmann |
introduced mk/dest_numeral/number for mk/dest_binum etc.
|
changeset |
files
|
| Wed, 13 Dec 2006 15:45:30 +0100 |
haftmann |
fixed syntax for bounded quantification
|
changeset |
files
|
| Wed, 13 Dec 2006 15:45:29 +0100 |
haftmann |
dropped superfluous header
|
changeset |
files
|
| Wed, 13 Dec 2006 14:56:50 +0100 |
krauss |
clarified error message
|
changeset |
files
|
| Wed, 13 Dec 2006 14:54:07 +0100 |
krauss |
nat type now has a size functin => no longer needed as special case
|
changeset |
files
|
| Wed, 13 Dec 2006 14:52:50 +0100 |
krauss |
simplified
|
changeset |
files
|
| Wed, 13 Dec 2006 14:52:30 +0100 |
wenzelm |
local_abbrev: proper fix/declare of local entities;
|
changeset |
files
|
| Wed, 13 Dec 2006 12:42:26 +0100 |
paulson |
Deleted the unused type argument of UVar
|
changeset |
files
|
| Wed, 13 Dec 2006 12:10:54 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 13 Dec 2006 12:07:43 +0100 |
krauss |
added IsarAdvanced/Functions
|
changeset |
files
|
| Wed, 13 Dec 2006 00:07:13 +0100 |
huffman |
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
|
changeset |
files
|
| Wed, 13 Dec 2006 00:02:53 +0100 |
huffman |
remove uses of scaleR infix syntax; add lemma Reals_number_of
|
changeset |
files
|
| Tue, 12 Dec 2006 21:25:14 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 12 Dec 2006 21:25:13 +0100 |
wenzelm |
add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);
|
changeset |
files
|
| Tue, 12 Dec 2006 20:50:23 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:32 +0100 |
wenzelm |
simplified unlocalize_mixfix;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:31 +0100 |
wenzelm |
removed is_class -- handled internally;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:30 +0100 |
wenzelm |
notation: Term.equiv_types;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:29 +0100 |
wenzelm |
abbrev: tuned signature;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:28 +0100 |
wenzelm |
tuned expand_term;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:27 +0100 |
wenzelm |
classified show/thus as prf_asm_goal, which is usually hilited in PG;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:26 +0100 |
wenzelm |
tuned expand_binds;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:25 +0100 |
wenzelm |
tuned error messages;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:24 +0100 |
wenzelm |
added equiv_types;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:23 +0100 |
wenzelm |
add_abbrev: tuned signature;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:22 +0100 |
wenzelm |
added expand_term_frees;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:21 +0100 |
wenzelm |
abbreviate: tuned signature;
|
changeset |
files
|
| Tue, 12 Dec 2006 20:49:19 +0100 |
wenzelm |
LocalTheory.abbrev;
|
changeset |
files
|
| Tue, 12 Dec 2006 17:29:26 +0100 |
huffman |
removed redundant constants and lemmas
|
changeset |
files
|
| Tue, 12 Dec 2006 17:15:42 +0100 |
huffman |
additions to HOL-Complex
|
changeset |
files
|
| Tue, 12 Dec 2006 16:20:57 +0100 |
paulson |
Removal of the "keep_types" flag: we always keep types!
|
changeset |
files
|
| Tue, 12 Dec 2006 12:03:46 +0100 |
wenzelm |
make SML/NJ happy;
|
changeset |
files
|
| Tue, 12 Dec 2006 11:57:30 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Tue, 12 Dec 2006 07:46:40 +0100 |
huffman |
consistent naming for FreeUltrafilterNat lemmas; cleaned up
|
changeset |
files
|
| Tue, 12 Dec 2006 07:13:06 +0100 |
huffman |
cleaned up; generalized some proofs
|
changeset |
files
|
| Tue, 12 Dec 2006 07:11:58 +0100 |
huffman |
fix assumptions on NSDERIV_quotient
|
changeset |
files
|
| Tue, 12 Dec 2006 04:37:25 +0100 |
huffman |
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
|
changeset |
files
|
| Tue, 12 Dec 2006 04:32:50 +0100 |
huffman |
generalize some theorems
|
changeset |
files
|
| Tue, 12 Dec 2006 04:31:34 +0100 |
huffman |
add type annotation
|
changeset |
files
|
| Tue, 12 Dec 2006 00:25:09 +0100 |
wenzelm |
read_xnum: return leading_zeros, radix;
|
changeset |
files
|
| Tue, 12 Dec 2006 00:25:05 +0100 |
wenzelm |
authentic syntax for Pls/Min/Bit;
|
changeset |
files
|
| Tue, 12 Dec 2006 00:25:03 +0100 |
wenzelm |
authentic syntax for Pls/Min/Bit;
|
changeset |
files
|
| Tue, 12 Dec 2006 00:25:02 +0100 |
wenzelm |
binary numerals: restricted to actual abstract syntax;
|
changeset |
files
|
| Tue, 12 Dec 2006 00:03:42 +0100 |
huffman |
Hyperreal/FrechetDeriv.thy
|
changeset |
files
|
| Tue, 12 Dec 2006 00:02:54 +0100 |
huffman |
theory of Frechet derivatives
|
changeset |
files
|
| Mon, 11 Dec 2006 21:41:05 +0100 |
wenzelm |
specials: include single quote;
|
changeset |
files
|
| Mon, 11 Dec 2006 21:41:03 +0100 |
wenzelm |
xstr: disallow backslashes;
|
changeset |
files
|
| Mon, 11 Dec 2006 21:39:28 +0100 |
wenzelm |
advanced translation functions: Proof.context;
|
changeset |
files
|
| Mon, 11 Dec 2006 21:39:26 +0100 |
wenzelm |
advanced translation functions: Proof.context;
|
changeset |
files
|
| Mon, 11 Dec 2006 19:05:25 +0100 |
wenzelm |
added improved versions of use_text/file (still inactive);
|
changeset |
files
|
| Mon, 11 Dec 2006 19:05:23 +0100 |
wenzelm |
added use_file;
|
changeset |
files
|
| Mon, 11 Dec 2006 19:05:20 +0100 |
wenzelm |
load secure.ML after symbol.ML, when default output is active;
|
changeset |
files
|
| Mon, 11 Dec 2006 16:58:19 +0100 |
webertj |
ordered lists instead of tables for resolving hyps; speedup
|
changeset |
files
|