Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+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.
updated
2007-07-19, by berghofe
Refer to major premise of induction rule via "thm_style prem1".
2007-07-19, by berghofe
Added named_thms antiquotation.
2007-07-19, by berghofe
Replaced "hand-made" files by generated files in Inductive/document.
2007-07-19, by berghofe
LaTeX code is now generated directly from theory files.
2007-07-19, by berghofe
LaTeX code is now generated directly from Even and Advanced theories.
2007-07-19, by berghofe
LaTeX code is now generated directly from theory file.
2007-07-19, by berghofe
DEEPEN: Use priority message channel for interim messages (not warnings).
2007-07-18, by aspinall
Direct priority and tracing channels properly.
2007-07-18, by aspinall
tidying using metis
2007-07-18, by paulson
fileident --- produce file identification based;
2007-07-17, by wenzelm
added ISABELLE_FILE_IDENT (command line for source file identification);
2007-07-17, by wenzelm
adapted TextIO.inputLine;
2007-07-17, by wenzelm
tuned comment;
2007-07-17, by wenzelm
avoid redundant variables in patterns (which made Alice vomit);
2007-07-17, by wenzelm
Full sort information by default.
2007-07-17, by paulson
Added hypotheses.
2007-07-17, by berghofe
Added clause for hypotheses to proof_of_xml function.
2007-07-17, by berghofe
use /usr/proj/polyml/polyml-5.1-test, which might be more stable;
2007-07-17, by wenzelm
reverted fun->recdef, since there are problems with induction rule
2007-07-17, by krauss
Pure theory setup.
2007-07-17, by wenzelm
Generic print mode.
2007-07-17, by wenzelm
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
2007-07-17, by wenzelm
simplified loading of ML files -- no static forward references;
2007-07-17, by wenzelm
moved print_translations from Pure.thy to Syntax/syn_trans.ML;
2007-07-17, by wenzelm
added General/print_mode.ML, pure_setup.ML;
2007-07-17, by wenzelm
tuned specifications;
2007-07-17, by wenzelm
use function package
2007-07-16, by krauss
more proofs
2007-07-16, by krauss
some interface cleanup
2007-07-16, by krauss
added lemma binding: accpI = accp.accI
2007-07-16, by krauss
updated
2007-07-16, by krauss
tidied using sledgehammer
2007-07-16, by paulson
tidied
2007-07-16, by paulson
tidied using sledgehammer
2007-07-16, by paulson
tidied using sledgehammer
2007-07-16, by paulson
clarified structure names
2007-07-16, by haftmann
added function for case certificates
2007-07-16, by haftmann
dropped outer ROOT structure for generated code
2007-07-16, by haftmann
tuned
2007-07-16, by haftmann
fixed SML/NJ int problem
2007-07-16, by haftmann
updated
2007-07-16, by haftmann
tuned;
2007-07-13, by wenzelm
updated
2007-07-12, by krauss
updated;
2007-07-12, by wenzelm
tuned signature;
2007-07-12, by wenzelm
sys_error;
2007-07-12, by wenzelm
simplified using Markup.get_int;
2007-07-12, by wenzelm
added skeleton for print_mode setup;
2007-07-12, by wenzelm
tuned spacing;
2007-07-12, by wenzelm
renamed PgipParser to OldPgipParser;
2007-07-12, by wenzelm
Parsing theory sources without execution (via keyword classification).
2007-07-12, by wenzelm
exported command_keyword;
2007-07-12, by wenzelm
command 'declare': proper thy_decl;
2007-07-12, by wenzelm
added get_string, get_int;
2007-07-12, by wenzelm
added ProofGeneral/pgip_parser.ML;
2007-07-12, by wenzelm
tuned error faces;
2007-07-11, by wenzelm
tries to solve goal via TrueI
2007-07-11, by nipkow
tuned markup;
2007-07-11, by wenzelm
replaced OuterLex.name_of by more sophisticated OuterLex.text_of;
2007-07-11, by wenzelm
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-11, by wenzelm
Buffer.markup;
2007-07-11, by wenzelm
removed ident, space;
2007-07-11, by wenzelm
added markup operation;
2007-07-11, by wenzelm
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-11, by wenzelm
Added entry for new inductive definition package.
2007-07-11, by berghofe
Proof terms for meta-conjunctions are now normalized before
2007-07-11, by berghofe
Added function norm_proof for normalizing the proof term
2007-07-11, by berghofe
Added function rew_proof (for pre-normalizing proofs).
2007-07-11, by berghofe
Function unify_consts moved from OldInductivePackage to PrimrecPackage.
2007-07-11, by berghofe
Adapted to new inductive definition package.
2007-07-11, by berghofe
Renamed accessible part for predicates to accp.
2007-07-11, by berghofe
renamed inductive2 to inductive.
2007-07-11, by berghofe
Renamed inductive2 to inductive.
2007-07-11, by berghofe
Hide member constant.
2007-07-11, by berghofe
Reverted renaming of "member".
2007-07-11, by berghofe
changed sources for HOL-Complex-Matrix
2007-07-11, by obua
Restored set notation in Multiset theory.
2007-07-11, by berghofe
added dummy makestring function
2007-07-11, by obua
Renamed inductive2 to inductive.
2007-07-11, by berghofe
fixed for SML/NJ
2007-07-11, by obua
Adapted to new inductive definition package.
2007-07-11, by berghofe
Adapted to changes in Accessible_Part theory.
2007-07-11, by berghofe
Function unify_consts moved from OldInductivePackage to PrimrecPackage.
2007-07-11, by berghofe
New wrapper for defining inductive sets with new inductive
2007-07-11, by berghofe
Old (co)inductive command is now replaced by (co)inductive_set.
2007-07-11, by berghofe
Reorganization due to introduction of inductive_set wrapper.
2007-07-11, by berghofe
Improved code generator for Collect.
2007-07-11, by berghofe
Renamed inductive2 to inductive.
2007-07-11, by berghofe
Fix nested PGIP messages. Update for schema simplifications.
2007-07-11, by aspinall
Moved unify_consts to PrimrecPackage.
2007-07-11, by berghofe
- Renamed inductive2 to inductive
2007-07-11, by berghofe
Adapted to changes in Predicate theory.
2007-07-11, by berghofe
Adapted to new inductive definition package.
2007-07-11, by berghofe
Renamed accessible part for predicates to accp.
2007-07-11, by berghofe
Track schema changes: merge messagecategory with area attributes
2007-07-11, by aspinall
bot is now a constant.
2007-07-11, by berghofe
Restored set notation.
2007-07-11, by berghofe
- Renamed inductive2 to inductive
2007-07-11, by berghofe
Track schema changes: remove cleardisplay, proofstate messages. Simplify attributes on cleardisplay, normalresponse.
2007-07-11, by aspinall
Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
2007-07-11, by aspinall
Renamed inductive2 to inductive.
2007-07-11, by berghofe
Adapted to new inductive definition package.
2007-07-11, by berghofe
New operations on tuples with specific arities.
2007-07-11, by berghofe
Adapted to changes in infrastructure for converting between
2007-07-11, by berghofe
rtrancl and trancl are now defined using inductive_set.
2007-07-11, by berghofe
Removed wf_implies_wfP and wfP_implies_wf from list of hints again.
2007-07-11, by berghofe
- Moved infrastructure for converting between sets and predicates
2007-07-11, by berghofe
Adapted to new package for inductive sets.
2007-07-11, by berghofe
Inserted definition of in_rel again (since member2 was removed).
2007-07-11, by berghofe
Added ML bindings for sup_fun_eq and sup_bool_eq.
2007-07-11, by berghofe
top and bot are now constants.
2007-07-11, by berghofe
Renamed inductive2 to inductive.
2007-07-11, by berghofe
acc is now defined using inductive_set.
2007-07-11, by berghofe
Added new package for inductive sets.
2007-07-11, by berghofe
Adapted to new inductive definition package.
2007-07-11, by berghofe
Adapted to changes in inductive definition package.
2007-07-11, by berghofe
tuned comment markup;
2007-07-11, by wenzelm
treat OuterLex.Error;
2007-07-11, by wenzelm
separated Malformed (symbolic char) from Error (bad input);
2007-07-11, by wenzelm
Output.escape_malformed;
2007-07-11, by wenzelm
added escape_malformed (failsafe);
2007-07-11, by wenzelm
Basic editing of theory sources.
2007-07-10, by wenzelm
tuned;
2007-07-10, by wenzelm
export html_mode, begin_document, end_document;
2007-07-10, by wenzelm
renamed XML.Rawtext to XML.Output;
2007-07-10, by wenzelm
export get_lexicons;
2007-07-10, by wenzelm
added kind_of;
2007-07-10, by wenzelm
Markup.enclose;
2007-07-10, by wenzelm
more markup for inner and outer syntax;
2007-07-10, by wenzelm
simplified funpow, untabify;
2007-07-10, by wenzelm
added Thy/thy_edit.ML;
2007-07-10, by wenzelm
added some markup for outer syntax;
2007-07-10, by wenzelm
clarified merge of module names
2007-07-10, by haftmann
now a monolithic module
2007-07-10, by haftmann
now works with SML/NJ
2007-07-10, by haftmann
tuned
2007-07-10, by haftmann
improvement for code names
2007-07-10, by haftmann
removed proof dependency on transitivity theorems
2007-07-10, by haftmann
moved lfp_induct2 here
2007-07-10, by haftmann
clarified import
2007-07-10, by haftmann
moved lfp_induct2 to Relation.thy
2007-07-10, by haftmann
moved some finite lemmas here
2007-07-10, by haftmann
moved finite lemmas to Finite_Set.thy
2007-07-10, by haftmann
added print_mode setup (from pretty.ML);
2007-07-10, by wenzelm
Markup.add_mode;
2007-07-10, by wenzelm
removed no_state markup -- produce empty state;
2007-07-10, by wenzelm
Markup.output;
2007-07-10, by wenzelm
moved source cascading from scan.ML to source.ML;
2007-07-10, by wenzelm
infixr || (more efficient);
2007-07-10, by wenzelm
moved print_mode setup for markup to markup.ML;
2007-07-10, by wenzelm
Markup.output;
2007-07-10, by wenzelm
use position.ML earlier;
2007-07-10, by wenzelm
Add widthN to signature
2007-07-10, by aspinall
cd ISABELLE_HOME/etc;
2007-07-10, by wenzelm
adjusted
2007-07-10, by haftmann
updated keywords
2007-07-10, by haftmann
simplified, tuned
2007-07-10, by haftmann
re-expanded paths
2007-07-10, by haftmann
replaced code generator framework for reflected cooper
2007-07-10, by haftmann
expanded fragile proof
2007-07-10, by haftmann
extended - convers now basic lcm properties also
2007-07-10, by haftmann
constant dvd now in class target
2007-07-10, by haftmann
moved lemma zdvd_period here
2007-07-10, by haftmann
introduced (auxiliary) class dvd_mod for more convenient code generation
2007-07-10, by haftmann
tuned;
2007-07-10, by wenzelm
nested source: explicit interactive flag for recover avoids duplicate errors;
2007-07-10, by wenzelm
tuned dead code;
2007-07-09, by wenzelm
use Position.file_of;
2007-07-09, by wenzelm
toplevel_source: interactive flag indicates intermittent error_msg;
2007-07-09, by wenzelm
Malformed token: error msg;
2007-07-09, by wenzelm
adapted OuterLex/T.source;
2007-07-09, by wenzelm
scan: changed treatment of malformed symbols, passed to next stage;
2007-07-09, by wenzelm
nested source: error msg passed to recover;
2007-07-09, by wenzelm
tuned signature;
2007-07-09, by wenzelm
replaced name by file (unquoted);
2007-07-09, by wenzelm
moved Path.position to Position.path;
2007-07-09, by wenzelm
proper position markup;
2007-07-09, by wenzelm
use position.ML after pretty.ML;
2007-07-09, by wenzelm
removed target RAW-ProofGeneral (impractical to maintain);
2007-07-09, by wenzelm
declare: disallow quote (") in names;
2007-07-09, by wenzelm
removed legacy ML file;
2007-07-09, by wenzelm
HOL-Complex-Matrix: fixed deps -- sort of;
2007-07-09, by wenzelm
adopted to new computing oracle and fixed bugs introduced by tuning
2007-07-09, by obua
added computing oracle support for HOL and numerals
2007-07-09, by obua
new version of computing oracle
2007-07-09, by obua
simplified writeln_fn;
2007-07-09, by wenzelm
prompt: plain string, not output;
2007-07-09, by wenzelm
type output = string indicates raw system output;
2007-07-09, by wenzelm
symbolic output: avoid empty blocks, 1 space for fbreak;
2007-07-08, by wenzelm
tuned;
2007-07-08, by wenzelm
thm tag: Markup.property list;
2007-07-08, by wenzelm
gensym: slightly more obscure prefix descreases probability of name clash;
2007-07-08, by wenzelm
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-08, by wenzelm
attribute tagged: single argument;
2007-07-08, by wenzelm
updated;
2007-07-08, by wenzelm
simplified Symtab;
2007-07-08, by wenzelm
renamed ML_exc to ML_exn;
2007-07-08, by wenzelm
Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
2007-07-08, by chaieb
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
2007-07-08, by chaieb
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
2007-07-08, by chaieb
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
2007-07-08, by chaieb
simplified/more robust print_state;
2007-07-08, by wenzelm
export mode_markup;
2007-07-08, by wenzelm
added markup for pretty printing;
2007-07-08, by wenzelm
Corrected erronus use of compiletime context to the runtime context
2007-07-08, by chaieb
make smlnj happy;
2007-07-07, by wenzelm
toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07, by wenzelm
toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07, by wenzelm
pretty_state: subgoal markup;
2007-07-07, by wenzelm
added markup_chunks;
2007-07-07, by wenzelm
added toplevel markup;
2007-07-07, by wenzelm
use markup.ML earlier;
2007-07-07, by wenzelm
removed obsolete disable_pr/enable_pr;
2007-07-07, by wenzelm
pretty_goals_aux: subgoal markup;
2007-07-07, by wenzelm
pr_goals: adapted Display.pretty_goals_aux;
2007-07-07, by wenzelm
export attribute;
2007-07-07, by wenzelm
pretty_sort/typ/term: markup;
2007-07-07, by wenzelm
pretty: markup for syntax/name of authentic consts;
2007-07-07, by wenzelm
depend on alist.ML, markup.ML;
2007-07-07, by wenzelm
markup: emit as control information -- no indent text;
2007-07-07, by wenzelm
added property conversions;
2007-07-07, by wenzelm
position: line and name;
2007-07-07, by wenzelm
moved markup.ML before position.ML;
2007-07-07, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
+30000
tip