Mercurial
Mercurial
>
repos
>
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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
Fundamental concepts.
2006-11-16, by wenzelm
add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);
2006-11-15, by wenzelm
tuned proofs;
2006-11-15, by wenzelm
replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;
2006-11-15, by wenzelm
replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;
2006-11-15, by wenzelm
dropping accidental self-imports
2006-11-15, by haftmann
corrected polymorphism check
2006-11-15, by haftmann
clarified code for building function equation system; explicit check of type discipline
2006-11-15, by haftmann
moved evaluation to Code_Generator.thy
2006-11-15, by haftmann
added filter_set; adaptions to more strict type discipline for code lemmas
2006-11-15, by haftmann
moved transitivity rules to Orderings.thy
2006-11-15, by haftmann
added transitivity rules, reworking of min/max lemmas
2006-11-15, by haftmann
dropped dependency on sets
2006-11-15, by haftmann
reworking of min/max lemmas
2006-11-15, by haftmann
added interpretation
2006-11-15, by haftmann
removed HOL_css
2006-11-15, by haftmann
added evaluation oracle
2006-11-15, by haftmann
replaced exists_fresh lemma with a version formulated with obtains;
2006-11-15, by urbanc
updated;
2006-11-15, by wenzelm
Auxiliary antiquotations for Isabelle manuals.
2006-11-15, by wenzelm
common antiquote_setup.ML;
2006-11-15, by wenzelm
Arity clauses are now produced only for types and type classes actually used.
2006-11-15, by paulson
converted to 'inductive2';
2006-11-14, by wenzelm
added for_simple_fixes, specification;
2006-11-14, by wenzelm
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
2006-11-14, by wenzelm
removed fix_frees interface;
2006-11-14, by wenzelm
converted to 'inductive2';
2006-11-14, by wenzelm
inductive: canonical specification syntax (flattened result only);
2006-11-14, by wenzelm
inductive2: canonical specification syntax;
2006-11-14, by wenzelm
InductivePackage.add_inductive_i: canonical argument order;
2006-11-14, by wenzelm
inductive2: canonical specification syntax;
2006-11-14, by wenzelm
Exported some names
2006-11-14, by schirmer
simplified Proof.theorem(_i) interface -- removed target support;
2006-11-14, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip