Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-112
+112
+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.
rewrite_proof: simplified simprocs (no name required);
2008-11-15, by wenzelm
Thm.proof_of returns proof_body;
2008-11-15, by wenzelm
refined notion of derivation, consiting of promises and proof_body;
2008-11-15, by wenzelm
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
2008-11-15, by wenzelm
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
2008-11-15, by wenzelm
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
2008-11-15, by wenzelm
name_of_thm: Proofterm.fold_proof_atoms;
2008-11-15, by wenzelm
Thm.proof_of returns proof_body;
2008-11-15, by wenzelm
clean: added HOL-Main;
2008-11-15, by wenzelm
rewrite_proof: simplified simprocs (no name required);
2008-11-15, by wenzelm
multithreading support for polyml-5.2 actually disabled -- as advertized;
2008-11-15, by wenzelm
Initial part of locale reimplementation.
2008-11-14, by ballarin
Made local_note_prefix public.
2008-11-14, by ballarin
re-educated guess
2008-11-14, by haftmann
namify and name_decl combinators
2008-11-14, by haftmann
Name.is_nothing
2008-11-14, by haftmann
lemmas about dom and minus / insert
2008-11-14, by haftmann
added length_unique operation for code generation
2008-11-14, by haftmann
updated generated files;
2008-11-13, by wenzelm
removed "includes" element (lost update?);
2008-11-13, by wenzelm
updated generated files;
2008-11-13, by wenzelm
added section "Explicit instantiation within a subgoal context";
2008-11-13, by wenzelm
renamed "Rules" to "Object-level rules";
2008-11-13, by wenzelm
more on basic tactics;
2008-11-13, by wenzelm
basic ML reference for tactics;
2008-11-13, by wenzelm
added section "Tactics";
2008-11-13, by wenzelm
more contributors;
2008-11-13, by wenzelm
separate section "Inspecting the syntax" for print_syntax;
2008-11-13, by wenzelm
misc tuning of inner syntax;
2008-11-13, by wenzelm
added inner lexical syntax, reusing outer one;
2008-11-13, by wenzelm
misc tuning;
2008-11-13, by wenzelm
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
2008-11-13, by wenzelm
more tuning of Pure grammer;
2008-11-13, by wenzelm
updated and elaborated Pure grammer;
2008-11-13, by wenzelm
added Pure grammer (from old ref manual);
2008-11-13, by wenzelm
mixfix annotations: verbatim for special symbols;
2008-11-13, by wenzelm
added section "The Pure grammar" (incomplete version, based on old ref manual);
2008-11-13, by wenzelm
added section "Priority grammars" (variant from old ref manual);
2008-11-13, by wenzelm
added section "Co-regularity of type classes and arities" (variant from old ref manual);
2008-11-13, by wenzelm
minor tuning (according to old ref manual);
2008-11-13, by wenzelm
misc tuning and rearrangement of section "Printing logical entities";
2008-11-13, by wenzelm
misc tuning and rearrangement of section "Printing logical entities";
2008-11-13, by wenzelm
fixed/tuned syntax for attribute "tagged";
2008-11-13, by wenzelm
added pretty printing options (from old ref manual);
2008-11-13, by wenzelm
separate chapter "Inner syntax --- the term language";
2008-11-13, by wenzelm
updated/refined types of Isar language elements, removed special LaTeX macros;
2008-11-13, by wenzelm
unified use of declaration environment with IsarImplementation;
2008-11-13, by wenzelm
ignore ThyOutput.source flag;
2008-11-13, by wenzelm
added bind_thm, bind_thms;
2008-11-13, by wenzelm
tuned section "Incorporating ML code";
2008-11-13, by wenzelm
tuned section "Oracles";
2008-11-13, by wenzelm
tuned section arrangement;
2008-11-13, by wenzelm
moved section "Proof method expressions" to proof chapter;
2008-11-13, by wenzelm
more on mixfix annotations (updated material from old ref manual);
2008-11-13, by wenzelm
tuned;
2008-11-13, by wenzelm
moved section "Document preparation" to front;
2008-11-13, by wenzelm
updated section "Markup via command tags";
2008-11-13, by wenzelm
renamed "formal comments" to "document comments";
2008-11-13, by wenzelm
renamed "formal comments" to "document comments";
2008-11-13, by wenzelm
tuned "Markup commands";
2008-11-13, by wenzelm
tuned intro of "Document preparation";
2008-11-13, by wenzelm
reworked "Defining Theories";
2008-11-13, by wenzelm
removed Assert.thy
2008-11-13, by haftmann
dropped superfluos eval_conv
2008-11-13, by haftmann
moved assert to Heap_Monad.thy
2008-11-13, by haftmann
simproc for let
2008-11-13, by haftmann
improved handling of !!/==> for eval and normalization
2008-11-13, by haftmann
proper name morphisms for locales
2008-11-13, by haftmann
consider prefixes for name bindings of simprocs (a first approximation)
2008-11-13, by haftmann
diagnostic output for name bindings
2008-11-13, by haftmann
Some modifications in code for proving arities to make it work for datatype
2008-11-13, by berghofe
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
2008-11-12, by krauss
restruced naming code in anticipation of introduction of name morphisms
2008-11-10, by haftmann
more verbose element printing
2008-11-10, by haftmann
clarified comment
2008-11-10, by haftmann
Added support for parametric datatypes.
2008-11-10, by berghofe
Streamlined functions for accessing information about atoms.
2008-11-10, by berghofe
Some more functions for accessing information about atoms.
2008-11-10, by berghofe
Made doc compatible with the system.
2008-11-10, by ballarin
clarified verbatim vs. typewriter
2008-11-10, by haftmann
using explicit interpretaton prefix in Name.binding (still on the surface)
2008-11-10, by haftmann
explicit interpretation prefix in Name.binding
2008-11-10, by haftmann
tuned
2008-11-10, by haftmann
exported codegen_preproc
2008-11-07, by haftmann
Minor cleanup.
2008-11-06, by ballarin
Keyword 'includes' gone.
2008-11-06, by ballarin
tuned
2008-11-06, by nipkow
added lemma
2008-11-06, by nipkow
Added second tiling example.
2008-11-06, by nipkow
cleaned
2008-11-06, by haftmann
tuned
2008-11-06, by haftmann
class morphism stemming from locale interpretation
2008-11-06, by haftmann
improved verbatim mechanism
2008-11-03, by haftmann
Theorem "_" is now stored with open derivation.
2008-10-31, by berghofe
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
2008-10-31, by berghofe
Replaced arbitrary by undefined.
2008-10-31, by berghofe
Dropped context element 'includes'.
2008-10-30, by ballarin
adapted to strict pattern discipline
2008-10-29, by haftmann
explicit check for pattern discipline before code translation
2008-10-29, by haftmann
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
2008-10-28, by ballarin
restored incremental code generation
2008-10-28, by haftmann
slightly tuned
2008-10-28, by haftmann
assert that no class parameter is used as constructor
2008-10-28, by haftmann
cleanup code default attribute
2008-10-28, by haftmann
removed includes
2008-10-28, by haftmann
making SMLNJ happy
2008-10-28, by haftmann
The metis method no longer fails because the theorem is too trivial
2008-10-28, by paulson
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-10-28, by ballarin
metis proof
2008-10-27, by paulson
New-style locale expressions with instantiation (new file expression.ML).
2008-10-27, by ballarin
Hide path in constant name (workaround).
2008-10-27, by ballarin
explicit history for equations; tuned
2008-10-27, by haftmann
less
more
|
(0)
-10000
-3000
-1000
-112
+112
+1000
+3000
+10000
+30000
tip