isabelle: Graph

simplified proofs
2007-01-22, by nipkow
Included ex/Fundefs.thy in HOL-ex session
2007-01-22, by krauss
* Preliminary implementation of tail recursion
2007-01-22, by krauss
Add location_of_position. Needs work elsewhere.
2007-01-22, by aspinall
Test askref
2007-01-22, by aspinall
Expose currently open file
2007-01-22, by aspinall
Sync location with pgip.rnc, fixing attribute names
2007-01-22, by aspinall
Add askrefs, setrefs, error_with_pos
2007-01-22, by aspinall
Comments
2007-01-22, by aspinall
Comment
2007-01-22, by aspinall
Add line_of, name_of destructors.
2007-01-22, by aspinall
Added lemma nat_size[simp]: "size (n::nat) = n"
2007-01-22, by krauss
tuned;
2007-01-22, by wenzelm
improved fact references: thmref;
2007-01-21, by wenzelm
added atomic, print_int;
2007-01-21, by wenzelm
tuned ML setup;
2007-01-21, by wenzelm
* ML in Isar: improved error reporting;
2007-01-21, by wenzelm
tuned;
2007-01-21, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2007-01-21, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2007-01-21, by wenzelm
tuned comments
2007-01-21, by wenzelm
simplified ML setup;
2007-01-21, by wenzelm
use_text: added name argument;
2007-01-21, by wenzelm
moved File.use to ML_Context.use;
2007-01-21, by wenzelm
use_text: added name argument;
2007-01-21, by wenzelm
Added simproc list_neq (prompted by an application)
2007-01-21, by nipkow
Added lists-as-multisets functions
2007-01-21, by nipkow
Simple and efficient binary numerals.
2007-01-20, by wenzelm
added HOL/ex/Binary.thy;
2007-01-20, by wenzelm
tuned ML setup;
2007-01-20, by wenzelm
* ML within Isar: antiquotations;
2007-01-20, by wenzelm
added @{theory};
2007-01-20, by wenzelm
added the_context_finished;
2007-01-20, by wenzelm
Toplevel.debug: coincide with Output.debugging;
2007-01-20, by wenzelm
ML tactic: proper context for compile and runtime;
2007-01-20, by wenzelm
tuned;
2007-01-20, by wenzelm
added @{simpset};
2007-01-20, by wenzelm
added is_finished_thy;
2007-01-20, by wenzelm
Output.debug: non-strict;
2007-01-20, by wenzelm
tuned ML setup;
2007-01-20, by wenzelm
added @{clasimpset};
2007-01-20, by wenzelm
added @{claset};
2007-01-20, by wenzelm
tuned;
2007-01-19, by wenzelm
tuned;
2007-01-19, by wenzelm
renamed Isar/isar_output.ML to Thy/thy_output.ML;
2007-01-19, by wenzelm
moved ML context stuff to from Context to ML_Context;
2007-01-19, by wenzelm
results: proper context;
2007-01-19, by wenzelm
tuned Scan.extend_lexicon;
2007-01-19, by wenzelm
renamed IsarOutput to ThyOutput;
2007-01-19, by wenzelm
moved parts to spec_parse.ML;
2007-01-19, by wenzelm
removed obsolete Method;
2007-01-19, by wenzelm
renamed IsarOutput to ThyOutput;
2007-01-19, by wenzelm
added various ML setup functions (from sign.ML, pure_thy.ML);
2007-01-19, by wenzelm
removed obsolete Attribute;
2007-01-19, by wenzelm
tuned signature;
2007-01-19, by wenzelm
renamed Isar/isar_output.ML to Thy/thy_output.ML;
2007-01-19, by wenzelm
tuned signature of extend_lexicon;
2007-01-19, by wenzelm
moved ML translation interfaces to isar_cmd.ML;
2007-01-19, by wenzelm
moved thm/thms to ml_context.ML;
2007-01-19, by wenzelm
moved inst from drule.ML to old_goals.ML;
2007-01-19, by wenzelm
tuned order;
2007-01-19, by wenzelm
renamed Isar/term_style.ML to Thy/term_style.ML;
2007-01-19, by wenzelm
renamed Isar/thy_header.ML to Thy/thy_header.ML;
2007-01-19, by wenzelm
ML context and antiquotations (material from context.ML);
2007-01-19, by wenzelm
Parsers for complex specifications (material from outer_parse.ML);
2007-01-19, by wenzelm
renamed Isar/isar_output.ML to Thy/thy_output.ML;
2007-01-19, by wenzelm
moved parts of OuterParse to SpecParse;
2007-01-19, by wenzelm
moved parts of OuterParse to SpecParse;
2007-01-19, by wenzelm
HOL-Lambda: usedir -m no_brackets;
2007-01-19, by wenzelm
simplified ML setup;
2007-01-19, by wenzelm
tuned;
2007-01-19, by wenzelm
renamed IsarOutput to ThyOutput;
2007-01-19, by wenzelm
updated;
2007-01-19, by wenzelm
moved ML context stuff to from Context to ML_Context;
2007-01-19, by wenzelm
renamed IsarOutput to ThyOutput;
2007-01-19, by wenzelm
interpreter for Finite_Set.finite added
2007-01-19, by webertj
reformatted to 80 chars/line
2007-01-19, by webertj
Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset.
2007-01-19, by chaieb
adapted ML context operations;
2007-01-19, by wenzelm
added generic_theory_of;
2007-01-19, by wenzelm
added 'declaration' command;
2007-01-19, by wenzelm
added 'declaration' command;
2007-01-19, by wenzelm
adapted ML context operations;
2007-01-19, by wenzelm
ML context: full generic context, tuned signature;
2007-01-19, by wenzelm
updated
2007-01-19, by wenzelm
Fix pgmlsymbolsoff
2007-01-18, by aspinall
tuned a bit the proofs
2007-01-17, by urbanc
correctled left/right following of another context in zipto.
2007-01-17, by dixon
induction rules for trancl/rtrancl expressed using subsets
2007-01-17, by paulson
Deleted mk_fol_type, since the constructors can be used directly
2007-01-17, by paulson
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
2007-01-17, by paulson
fixed typo introduced by me
2007-01-16, by urbanc
changed dictionary representation to explicit classrel witnesses
2007-01-16, by haftmann
reverted order of classrels
2007-01-16, by haftmann
cleanup
2007-01-16, by haftmann
formalisation of Crary's chapter on logical relations
2007-01-16, by urbanc
added capabilities to handle mutual inductions
2007-01-16, by urbanc
refined and added example for ExecutableRat
2007-01-16, by haftmann
introduced binding concept
2007-01-16, by haftmann
slight cleanup
2007-01-16, by haftmann
renamed locale partial_order to order
2007-01-16, by haftmann
refined and added example for ExecutableRat
2007-01-16, by haftmann
updated keywords
2007-01-16, by haftmann
added sections on mutual induction and patterns
2007-01-15, by krauss
optimized translation of HO problems
2007-01-14, by paulson
Reverted to structure representation with records.
2007-01-12, by ballarin
more term inspection
2007-01-12, by haftmann
introduced binding concept
2007-01-12, by haftmann
adjusted manual
2007-01-12, by haftmann
well-founded relations for the integers
2007-01-11, by paulson
updated to mention the automatic unfolding of constants
2007-01-11, by webertj
removed NameSpace.split -- use qualifier/base instead;
2007-01-10, by wenzelm
fixed exit: proper type check of state;
2007-01-10, by wenzelm
tuned
2007-01-10, by webertj
minor comment change
2007-01-10, by webertj
no unfolding necessary anymore (refute does that automatically now)
2007-01-10, by webertj
improved case patterns
2007-01-10, by haftmann
added undefined in cases
2007-01-10, by haftmann
named preprocessorts
2007-01-09, by haftmann
cleanup
2007-01-09, by haftmann
activated new class code
2007-01-09, by haftmann
handling for "undefined" in case expressions
2007-01-09, by haftmann
named preprocessors
2007-01-09, by haftmann
The "of 1, simplified" stopped working some time ago, leaving these simprules
2007-01-09, by paulson
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
2007-01-09, by paulson
simplified the resoution proofs
2007-01-09, by paulson
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
2007-01-09, by aspinall
Add info fatality for error messages.
2007-01-09, by aspinall
Add informfileoutdated and completed flag. This makes the PGIP messages match the Broker states.
2007-01-09, by aspinall
slight cleanups
2007-01-09, by haftmann
improved names
2007-01-09, by haftmann
proper node names
2007-01-09, by haftmann
slight cleanup
2007-01-09, by haftmann
improved variable name handling
2007-01-09, by haftmann
moved variable environments here
2007-01-09, by haftmann
moved a lot to codegen_func.ML
2007-01-09, by haftmann
typo
2007-01-09, by haftmann
added map_abs_vars
2007-01-09, by haftmann
tuned signature;
2007-01-08, by wenzelm
print functions for typs and terms added
2007-01-07, by webertj
Be more chatty in PGIP file operations.
2007-01-07, by aspinall
A few lemmas about relative primes when dividing trough gcd
2007-01-06, by chaieb
A few theorems on integer divisibily.
2007-01-06, by chaieb
Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever
2007-01-05, by paulson
reverted to v1.60 (PolyML 4.1.3 still has the wrong signature for Array.modifyi)
2007-01-05, by webertj
added codegen_func.ML
2007-01-05, by haftmann
non-layout-sensitive syntax for Haskell
2007-01-05, by haftmann
some cleanup
2007-01-05, by haftmann
primitive definitions are always eta-expanded
2007-01-05, by haftmann
added block_enclose
2007-01-05, by haftmann
added CodeEval
2007-01-05, by haftmann
dealing with ml_string and char instances
2007-01-05, by haftmann
dealing with ml_string combinators
2007-01-05, by haftmann
adaptions
2007-01-05, by haftmann
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
2007-01-05, by wenzelm
RAW-ProofGeneral: more dependencies;
2007-01-05, by wenzelm
Proof.context now sent to watcher and used in type inference step of proof reconstruction
2007-01-05, by paulson
tuned msg;
2007-01-04, by wenzelm
removed obsolete ProofGeneral/syntax_standalone.ML;
2007-01-04, by wenzelm
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
2007-01-04, by wenzelm
added mk_simproc': tuned interface;
2007-01-04, by wenzelm
clarification
2007-01-04, by haftmann
dropped function theorems are considered as deleted
2007-01-04, by haftmann
examples for evaluation oracle
2007-01-04, by haftmann
fixed eval oracle
2007-01-04, by haftmann
Be more chatty in PGIP file operations.proof_general_pgip.ML
2007-01-04, by aspinall
broken error handling for command syntax -- reverted to revision 1.9;
2007-01-04, by wenzelm
Use warning fatality
2007-01-04, by aspinall
Add warning fatality
2007-01-04, by aspinall
improvements to proof reconstruction. Some files loaded in a different order
2007-01-04, by paulson
using Array.modifyi (no functional change)
2007-01-04, by webertj
run as RAW session;
2007-01-04, by wenzelm
removed obsolete option -C;
2007-01-04, by wenzelm
removed obsolete Pure-copied target;
2007-01-04, by wenzelm
updated manual
2007-01-04, by haftmann
updated manual
2007-01-04, by haftmann
obsolete sign_of calls removed
2007-01-04, by webertj
fixed output
2007-01-04, by haftmann
different handling of eta expansion
2007-01-04, by haftmann
eta-expansion now only to common maximum number of arguments
2007-01-04, by haftmann
clarified code
2007-01-04, by haftmann
more term examples
2007-01-04, by haftmann
eliminated Option.app
2007-01-04, by haftmann
constants are unfolded, universal quantifiers are stripped, some minor changes
2007-01-04, by webertj
Fix error reporting in Emacs to also match Isar command failure exactly.
2007-01-03, by aspinall
Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
2007-01-03, by aspinall
Expose command failure recovery code for top level.
2007-01-03, by aspinall
Selected functions from syntax module
2007-01-03, by aspinall
x-symbol is no longer switched off in the ATP linkup
2007-01-03, by paulson
Improvements to proof reconstruction. Now "fixes" is inserted
2007-01-03, by paulson
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
2007-01-03, by paulson
first version of structured proof reconstruction
2007-01-03, by paulson