isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle