isabelle: Graph

Adapted to new nominal_primrec command.
2006-11-27, by berghofe
Added nominal_primrec.ML
2006-11-27, by berghofe
Implemented new "nominal_primrec" command for defining
2006-11-27, by berghofe
Additional information about nominal datatypes (descriptor,
2006-11-27, by berghofe
converted legacy ML scripts;
2006-11-26, by wenzelm
Remove add_master_files which stripped paths for retracted files. Emacs PG already supports full paths here.
2006-11-26, by aspinall
* Pure: syntax constant for foo (binder) is called foo_binder;
2006-11-26, by wenzelm
extend_trtab: allow identical trfuns to be overwritten;
2006-11-26, by wenzelm
tuned;
2006-11-26, by wenzelm
Binder: syntax const is determined by binder_name, not its syntax;
2006-11-26, by wenzelm
simplified consts: no auxiliary params, sane mixfix syntax;
2006-11-26, by wenzelm
abbrevs: no result;
2006-11-26, by wenzelm
added export_(standard_)morphism;
2006-11-26, by wenzelm
Element.map_ctxt_attrib;
2006-11-26, by wenzelm
abbrevs: no result;
2006-11-26, by wenzelm
added map_ctxt_attrib;
2006-11-26, by wenzelm
abbrevs: no result;
2006-11-26, by wenzelm
added morh_result, the_inductive, add_inductive_global;
2006-11-26, by wenzelm
InductivePackage.add_inductive_global;
2006-11-26, by wenzelm
updated (binder) syntax/notation;
2006-11-26, by wenzelm
tuned morphisms;
2006-11-24, by wenzelm
added export_morphism;
2006-11-24, by wenzelm
simultaneous fact morphism;
2006-11-24, by wenzelm
added type_map;
2006-11-24, by wenzelm
added cterm_rule;
2006-11-24, by wenzelm
fake predeclaration of structure ProofContext;
2006-11-24, by wenzelm
added export_morphism;
2006-11-24, by wenzelm
ProofContext.init;
2006-11-24, by wenzelm
Comment: see RFC 2396 for relative URI syntax.
2006-11-24, by aspinall
Send full paths in PGIP version of file loaded/retracted messages
2006-11-24, by aspinall
Conversion of "equal" to "=" for TSTP format; big tidy-up
2006-11-24, by paulson
Lemma "fundef_default_value" uses predicate instead of set.
2006-11-24, by krauss
The function package declares the [code] attribute automatically again.
2006-11-24, by krauss
exported mk_base_funs for use by size-change tools
2006-11-24, by krauss
ATP linkup now generates "new TPTP" rather than "old TPTP"
2006-11-24, by paulson
more careful declaration of "inducts";
2006-11-23, by wenzelm
tuned;
2006-11-23, by wenzelm
prefer Proof.context over Context.generic;
2006-11-23, by wenzelm
prefer Proof.context over Context.generic;
2006-11-23, by wenzelm
tuned proofs;
2006-11-23, by wenzelm
Accept URLs of form file:/home... also.
2006-11-23, by aspinall
prefer antiquotations over LaTeX macros;
2006-11-23, by wenzelm
updated;
2006-11-23, by wenzelm
renamed Args.Name to Args.Text;
2006-11-23, by wenzelm
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-23, by wenzelm
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-23, by wenzelm
Morphism.thm_morphism;
2006-11-23, by wenzelm
renamed Name value to Text, which is *not* a name in terms of morphisms;
2006-11-23, by wenzelm
removed obsolete alphanum;
2006-11-23, by wenzelm
str_of_char: improved output of non-printables;
2006-11-23, by wenzelm
added head_name_of;
2006-11-23, by wenzelm
added name/var/typ/term/thm_morphism;
2006-11-23, by wenzelm
declarations: pass morphism (dummy);
2006-11-23, by wenzelm
added ISABELLE_IDENTIFIER;
2006-11-23, by wenzelm
ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;
2006-11-23, by wenzelm
fixed some typos
2006-11-23, by urbanc
tuned the proof of the strong induction principle
2006-11-23, by urbanc
typo in comment fixed
2006-11-23, by webertj
Add retractfile to supported pgip commands
2006-11-23, by aspinall
PGIP: add retractfile. Be stricter in file open/close protocol.
2006-11-23, by aspinall
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
2006-11-23, by wenzelm
moved ML identifiers to structure ML_Syntax;
2006-11-23, by wenzelm
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
simplified Proof.theorem(_i) interface;
2006-11-14, by wenzelm
antiquotation theory: plain Theory.requires, no peeking at ThyInfo;
2006-11-14, by wenzelm
simplified Proof.theorem(_i) interface;
2006-11-14, by wenzelm
tuned antiquotation theory;
2006-11-14, by wenzelm
value restriction
2006-11-14, by haftmann
removed old cygwin wrappers;
2006-11-14, by wenzelm
declare_constraints: reset constraint on dummyS;
2006-11-14, by wenzelm
removed Isar/isar_thy.ML;
2006-11-14, by wenzelm
added dummyS;
2006-11-14, by wenzelm
removed legacy read/cert/string_of;
2006-11-14, by wenzelm
recdef_tc(_i): local_theory interface via Specification.theorem_i;
2006-11-14, by wenzelm
incorporated IsarThy into IsarCmd;
2006-11-14, by wenzelm
removed theorem(_i);
2006-11-14, by wenzelm
upd
2006-11-13, by haftmann
atbroy51 broke down, switch to atbroy9
2006-11-13, by kleing
updated
2006-11-13, by krauss
antiquotation "theory": proper output, only check via ThyInfo.theory;
2006-11-13, by wenzelm
tuned;
2006-11-13, by wenzelm
added antiquotation @{theory name};
2006-11-13, by wenzelm
fixed comment -- oops;
2006-11-13, by wenzelm
adjusted to new fun''
2006-11-13, by haftmann
*** empty log message ***
2006-11-13, by haftmann
added antiquotation theory
2006-11-13, by haftmann
cleaned up
2006-11-13, by haftmann
added theory antiquotation
2006-11-13, by haftmann
combinator for overwriting changes with warning
2006-11-13, by haftmann
added higher-order combinators for structured results
2006-11-13, by haftmann
adjusted name in generated code
2006-11-13, by haftmann
dropped LOrder dependency
2006-11-13, by haftmann
moved upwars in HOL theory graph
2006-11-13, by haftmann
added thy dependencies
2006-11-13, by haftmann
PreList = Main - List
2006-11-13, by haftmann
introduces preorders
2006-11-13, by haftmann
dropped Inductive dependency
2006-11-13, by haftmann
dropped Typedef dependency
2006-11-13, by haftmann
added LOrder dependency
2006-11-13, by haftmann
tuned ml antiquotations
2006-11-13, by haftmann
adjusted
2006-11-13, by haftmann
tuned
2006-11-13, by haftmann
added tt tag
2006-11-13, by haftmann
auto_term => lexicographic_order
2006-11-13, by krauss
updated
2006-11-13, by krauss
replaced "auto_term" by the simpler method "relation", which does not try
2006-11-13, by krauss
added fresh_prodD, which is included fresh_prodD into mksimps setup;
2006-11-13, by wenzelm
added lexicographic_order.ML to makefile
2006-11-13, by krauss
image_constant_conv no longer [simp]
2006-11-12, by nipkow
instantiate: tuned indentity case;
2006-11-12, by wenzelm
removed dead code;
2006-11-12, by wenzelm
mk_atomize: careful matching against rules admits overloading;
2006-11-12, by wenzelm
started reorgnization of lattice theories
2006-11-12, by nipkow
Added in is_fol_thms.
2006-11-11, by mengj
level: do not account for local theory blocks (relevant for document preparation);
2006-11-11, by wenzelm
local 'end': no default tags;
2006-11-11, by wenzelm
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
2006-11-11, by wenzelm
removed obsolete context;
2006-11-11, by wenzelm
turned 'context' into plain thy_decl, discontinued thy_switch;
2006-11-11, by wenzelm
tuned proofs;
2006-11-11, by wenzelm
updated local theory targets;
2006-11-11, by wenzelm