Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+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.
fulfill_proof/thm_proof: commuted lazyness;
2008-11-18, by wenzelm
fulfill_proof/thm_proof: commuted lazyness;
2008-11-18, by wenzelm
removed lemmas called lemma1 and lemma2
2008-11-18, by krauss
force_proofs after cumulative use_thys;
2008-11-18, by wenzelm
signed_string_of_int for priorities;
2008-11-18, by wenzelm
added force_proofs;
2008-11-18, by wenzelm
added force_proofs (based on thms ever passed through enter_thms);
2008-11-18, by wenzelm
tuned;
2008-11-18, by wenzelm
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
2008-11-18, by wenzelm
moved table of standard Isabelle symbols to isar-ref manual;
2008-11-18, by wenzelm
added isabelle-implementation manual;
2008-11-18, by wenzelm
disabled threads -- as advertized;
2008-11-18, by wenzelm
changes by Fabian Immler:
2008-11-18, by wenzelm
Code for switching to new locales.
2008-11-18, by ballarin
add_thmss
2008-11-18, by ballarin
Activate elements moved to element.ML.
2008-11-18, by ballarin
finish: force proofs;
2008-11-18, by wenzelm
finish_proof: undefined promises may occur here;
2008-11-17, by wenzelm
tuned promise/fullfill;
2008-11-17, by wenzelm
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
2008-11-17, by wenzelm
removed Induct/Mutil.thy -- the file has been moved to AFP;
2008-11-17, by wenzelm
simplified thm_deps -- no need to build a graph datastructure;
2008-11-17, by wenzelm
removed Induct/Mutil.thy -- the file has been moved to AFP;
2008-11-17, by wenzelm
-> AFP
2008-11-17, by nipkow
tuned unfold_locales invocation
2008-11-17, by haftmann
explicit name morphism function for locale interpretation
2008-11-17, by haftmann
Name.name_with_prefix (temporarily)
2008-11-17, by haftmann
adjusted locale signature to *_cmd convention
2008-11-17, by haftmann
whitespace tuning
2008-11-17, by haftmann
Generic activation of locales.
2008-11-17, by ballarin
proof_body/pthm: removed redundant types field;
2008-11-16, by wenzelm
put_name/thm_proof: promises are filled with fulfilled proofs;
2008-11-16, by wenzelm
proof_body/pthm: removed redundant types field;
2008-11-16, by wenzelm
clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-16, by wenzelm
- Corrected order of quantification over Frees.
2008-11-16, by berghofe
Frees in PThms are now quantified in the order of their appearance in the
2008-11-16, by berghofe
adapted PThm and MinProof;
2008-11-15, by wenzelm
retrieve thm deps from proof_body;
2008-11-15, by wenzelm
retrieve thm deps from proof_body;
2008-11-15, by wenzelm
adapted PThm;
2008-11-15, by wenzelm
proof_of_term: removed obsolete disambiguisation table;
2008-11-15, by wenzelm
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
slightly tuned
2008-10-27, by haftmann
added rudimentary code generation
2008-10-27, by haftmann
sup_bot and inf_top
2008-10-27, by haftmann
Extension of interface: declarations_of.
2008-10-27, by ballarin
simplified user-defined class syntax
2008-10-24, by haftmann
more clever module names for code generation
2008-10-24, by haftmann
"fun" gained a more uniform status
2008-10-24, by haftmann
simplified syntax for class parameters
2008-10-24, by haftmann
tuned
2008-10-24, by haftmann
new classes "top" and "bot"
2008-10-24, by haftmann
tuned proof
2008-10-24, by haftmann
more clever module name aliasses for code generation
2008-10-24, by haftmann
"arbitrary" merely abbreviates undefined
2008-10-24, by haftmann
subst is a proper axiom again
2008-10-24, by haftmann
updated
2008-10-24, by haftmann
explicit namings for generated code
2008-10-24, by haftmann
Thm.get_def;
2008-10-23, by wenzelm
Thm.def_name;
2008-10-23, by wenzelm
multithreading support only for polyml-5.2.1 or later;
2008-10-23, by wenzelm
renamed get_axiom_i to axiom, removed obsolete get_axiom;
2008-10-23, by wenzelm
renamed Thm.get_axiom_i to Thm.axiom;
2008-10-23, by wenzelm
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
2008-10-23, by wenzelm
adapted Susp.peek;
2008-10-23, by wenzelm
thread-safe version, with non-critical evaluation;
2008-10-23, by wenzelm
do not open Susp;
2008-10-23, by wenzelm
switched parallel sessions to polyml-5.2.1;
2008-10-23, by wenzelm
fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
2008-10-23, by wenzelm
updated to 5.2.1;
2008-10-22, by wenzelm
prove_instantiation_exit combinators
2008-10-22, by haftmann
added meet_sort_typ
2008-10-22, by haftmann
tuned
2008-10-22, by haftmann
code identifier namings are no longer imperative
2008-10-22, by haftmann
tuned typedef interface
2008-10-22, by haftmann
slightly tuned
2008-10-22, by haftmann
fixed
2008-10-22, by haftmann
less ambitious default for JEDIT_JAVA_OPTIONS;
2008-10-21, by wenzelm
JEDIT_OPTIONS: moved -settings to interface script (more robust);
2008-10-21, by wenzelm
make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;
2008-10-21, by wenzelm
Added nominal_inductive2.
2008-10-21, by berghofe
Example for using the generalized version of nominal_inductive.
2008-10-21, by berghofe
Added theory W.
2008-10-21, by berghofe
More general, still experimental version of nominal_inductive for
2008-10-21, by berghofe
Added nominal_inductive2.ML
2008-10-21, by berghofe
added jEdit settings;
2008-10-21, by wenzelm
tuned usage line;
2008-10-21, by wenzelm
Isabelle/jEdit interface wrapper.
2008-10-21, by wenzelm
join results in isolation;
2008-10-21, by wenzelm
join_results: allow CRITICAL join of finished futures;
2008-10-21, by wenzelm
Future.join_result;
2008-10-21, by wenzelm
added Future.enabled check;
2008-10-21, by wenzelm
ThyOutput: export some auxiliary operations;
2008-10-21, by wenzelm
fixed proof
2008-10-20, by nipkow
added lemmas
2008-10-20, by nipkow
Names of variables in perm_eqs are now chosen more carefully to avoid
2008-10-19, by berghofe
- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
2008-10-19, by berghofe
datatype_codegen now checks name of result type of constructor
2008-10-19, by berghofe
run a program in a modified environment;
2008-10-19, by wenzelm
reactivated HOL-Matrix;
2008-10-17, by wenzelm
tuned
2008-10-17, by haftmann
filled remaining gaps
2008-10-17, by haftmann
added type antiquotation
2008-10-17, by haftmann
tuned;
2008-10-16, by wenzelm
added dep for Concurrent/ROOT.ML;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
removed Locales;
2008-10-16, by wenzelm
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-16, by wenzelm
added translations for SORT_CONSTRAINT
2008-10-16, by wenzelm
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added make;
2008-10-16, by wenzelm
maintain sort occurrences of declared terms;
2008-10-16, by wenzelm
added weaken_sorts;
2008-10-16, by wenzelm
added make, minimal_sorts;
2008-10-16, by wenzelm
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
2008-10-16, by wenzelm
added check_shyps, which reject pending sort hypotheses;
2008-10-16, by wenzelm
Drule.norm_hhf_eqs;
2008-10-16, by wenzelm
prove_common: include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added rules for sort_constraint, include in norm_hhf_eqs;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
avoid accidental dependency of automated proof on sort equiv;
2008-10-16, by wenzelm
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
2008-10-16, by wenzelm
avoid CRITICAL with_path;
2008-10-16, by wenzelm
rewrite more proofs in Isar style
2008-10-16, by huffman
Removed ex/Locales.thy.
2008-10-16, by ballarin
More occurrences of 'includes' gone.
2008-10-16, by ballarin
Removed outdated locales tutorial.
2008-10-16, by ballarin
correct rounding
2008-10-16, by haftmann
circumvent some TeX problem
2008-10-16, by haftmann
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip