isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

Send full paths in PGIP version of file loaded/retracted messages
2006-11-24, by aspinall
Conversion of "equal" to "=" for TSTP format; big tidy-up
2006-11-24, by paulson
Lemma "fundef_default_value" uses predicate instead of set.
2006-11-24, by krauss
The function package declares the [code] attribute automatically again.
2006-11-24, by krauss
exported mk_base_funs for use by size-change tools
2006-11-24, by krauss
ATP linkup now generates "new TPTP" rather than "old TPTP"
2006-11-24, by paulson
more careful declaration of "inducts";
2006-11-23, by wenzelm
tuned;
2006-11-23, by wenzelm
prefer Proof.context over Context.generic;
2006-11-23, by wenzelm
prefer Proof.context over Context.generic;
2006-11-23, by wenzelm
tuned proofs;
2006-11-23, by wenzelm
Accept URLs of form file:/home... also.
2006-11-23, by aspinall
prefer antiquotations over LaTeX macros;
2006-11-23, by wenzelm
updated;
2006-11-23, by wenzelm
renamed Args.Name to Args.Text;
2006-11-23, by wenzelm
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-23, by wenzelm
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-23, by wenzelm
Morphism.thm_morphism;
2006-11-23, by wenzelm
renamed Name value to Text, which is *not* a name in terms of morphisms;
2006-11-23, by wenzelm
removed obsolete alphanum;
2006-11-23, by wenzelm
str_of_char: improved output of non-printables;
2006-11-23, by wenzelm
added head_name_of;
2006-11-23, by wenzelm
added name/var/typ/term/thm_morphism;
2006-11-23, by wenzelm
declarations: pass morphism (dummy);
2006-11-23, by wenzelm
added ISABELLE_IDENTIFIER;
2006-11-23, by wenzelm
ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;
2006-11-23, by wenzelm
fixed some typos
2006-11-23, by urbanc
tuned the proof of the strong induction principle
2006-11-23, by urbanc
typo in comment fixed
2006-11-23, by webertj
Add retractfile to supported pgip commands
2006-11-23, by aspinall
PGIP: add retractfile. Be stricter in file open/close protocol.
2006-11-23, by aspinall
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
2006-11-23, by wenzelm
moved ML identifiers to structure ML_Syntax;
2006-11-23, by wenzelm
added morph_ctxt, morph_witness;
2006-11-23, by wenzelm
replaced map_values by morph_values;
2006-11-23, by wenzelm
moved string_of_pair/list/option to structure ML_Syntax;
2006-11-23, by wenzelm
moved ML syntax operations to structure ML_Syntax;
2006-11-23, by wenzelm
Basic ML syntax operations.
2006-11-23, by wenzelm
Abstract morphisms on formal entities.
2006-11-23, by wenzelm
added morphism.ML, General/ml_syntax.ML;
2006-11-23, by wenzelm
renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;
2006-11-23, by wenzelm
removed dead code;
2006-11-23, by wenzelm
Add doccomment; rename litcomment -> doccomment
2006-11-23, by aspinall
* settings: ML_IDENTIFIER includes the Isabelle version identifier;
2006-11-22, by wenzelm
Consolidation of code to "blacklist" unhelpful theorems, including record
2006-11-22, by paulson
ML_IDENTIFIER includes Isabelle version;
2006-11-22, by wenzelm
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
2006-11-22, by wenzelm
consts: ProofContext.set_stmt true -- avoids naming of local thms;
2006-11-22, by wenzelm
init: enter inner statement mode, which prevents local notes from being named internally;
2006-11-22, by wenzelm
more careful declaration of "intros" as Pure.intro;
2006-11-22, by wenzelm
Fix to local file URI syntax. Add first part of lexicalstructure command support.
2006-11-22, by aspinall
completed class parameter handling in axclass.ML
2006-11-22, by haftmann
added Isar syntax for adding parameters to axclasses
2006-11-22, by haftmann
forced name prefix for class operations
2006-11-22, by haftmann
example tuned
2006-11-22, by haftmann
no explicit check for theory Nat
2006-11-22, by haftmann
added code lemmas
2006-11-22, by haftmann
does not import Hilber_Choice any longer
2006-11-22, by haftmann
cleanup
2006-11-22, by haftmann
incorporated structure HOList into HOLogic
2006-11-22, by haftmann
dropped eq const
2006-11-22, by haftmann
removed Extraction dependency
2006-11-22, by haftmann
final draft
2006-11-22, by haftmann
made SML/NJ happy;
2006-11-21, by wenzelm
theorem(_i): note assms of statement;
2006-11-21, by wenzelm
removed obsolete simple_note_thms;
2006-11-21, by wenzelm
added assmsN;
2006-11-21, by wenzelm
* Isar: the assumptions of a long theorem statement are available as assms;
2006-11-21, by wenzelm
activated x86_64-linux;
2006-11-21, by wenzelm
renamed Proof.put_thms_internal to Proof.put_thms;
2006-11-21, by wenzelm
simplified Proof.theorem(_i);
2006-11-21, by wenzelm
added stmt mode, which affects naming/indexing of local facts;
2006-11-21, by wenzelm
simplified theorem(_i);
2006-11-21, by wenzelm
notes: proper kind;
2006-11-21, by wenzelm
notes: proper kind;
2006-11-21, by wenzelm
removed kind attribs;
2006-11-21, by wenzelm
moved theorem kinds from PureThy to Thm;
2006-11-21, by wenzelm
moved theorem kinds from PureThy to Thm;
2006-11-21, by wenzelm
LocalTheory.notes/defs: proper kind;
2006-11-21, by wenzelm
LocalTheory.axioms/notes/defs: proper kind;
2006-11-21, by wenzelm
simplified Proof.theorem(_i);
2006-11-21, by wenzelm
LocalTheory.axioms/notes/defs: proper kind;
2006-11-21, by wenzelm
Optimized class_pairs for the common case of no subclasses
2006-11-21, by paulson
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
2006-11-21, by paulson
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
2006-11-21, by paulson
run poly-4.9.1 as stable and poly-4.2.0 as experimental on at
2006-11-21, by kleing
removed legacy ML setup;
2006-11-21, by wenzelm
converted legacy ML scripts;
2006-11-21, by wenzelm
converted legacy ML scripts;
2006-11-20, by wenzelm
HOL-Prolog: converted legacy ML scripts;
2006-11-20, by wenzelm
start at-sml earlier and on different machine, remove sun-sml test (takes too long)
2006-11-20, by kleing
HOL-Algebra: converted legacy ML scripts;
2006-11-19, by wenzelm
profiling disabled
2006-11-19, by webertj
code thms for classops violating type discipline ignored
2006-11-18, by haftmann
cleanup
2006-11-18, by haftmann
added instance for class size
2006-11-18, by haftmann
added combinators and lemmas
2006-11-18, by haftmann
using class instance
2006-11-18, by haftmann
dvd_def now with object equality
2006-11-18, by haftmann
op div/op mod now named without leading op
2006-11-18, by haftmann
workaround for definition violating type discipline
2006-11-18, by haftmann
moved dvd stuff to theory Divides
2006-11-18, by haftmann
re-eliminated thm trichotomy
2006-11-18, by haftmann
power is now a class
2006-11-18, by haftmann
tuned
2006-11-18, by haftmann
clarified module dependencies
2006-11-18, by haftmann
div is now a class
2006-11-18, by haftmann
reduced verbosity
2006-11-18, by haftmann
adjustments for class package
2006-11-18, by haftmann
added an intro lemma for freshness of products; set up
2006-11-17, by urbanc
more robust syntax for definition/abbreviation/notation;
2006-11-17, by wenzelm
'notation': more robust 'and' list;
2006-11-17, by wenzelm
updated;
2006-11-17, by wenzelm
added Isar.goal;
2006-11-17, by wenzelm
added where_;
2006-11-17, by wenzelm
add lemmas LIM_zero_iff, LIM_norm_zero_iff
2006-11-16, by huffman
Includes type:sort constraints in its code to collect predicates in axiom clauses.
2006-11-16, by paulson
Now includes only types used to instantiate overloaded constants in arity clauses
2006-11-16, by paulson
added General/basics.ML;
2006-11-16, by wenzelm
moved some fundamental concepts to General/basics.ML;
2006-11-16, by wenzelm