| #
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
| #
839d9ae3 |
|
26-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
|
| #
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
53f968f4 |
|
01-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
| #
cff2e75b |
|
08-Apr-2015 |
wenzelm <none@none> |
proper context for Object_Logic operations;
|
| #
90c1e718 |
|
06-Mar-2015 |
wenzelm <none@none> |
proper context;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
45f9fa0b |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
9067b570 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems;
modernized module name and setup;
|
| #
f5593ebf |
|
20-Mar-2014 |
wenzelm <none@none> |
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
|
| #
147d4ad6 |
|
07-Mar-2014 |
blanchet <none@none> |
tuning
|
| #
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
|
| #
1d64bfe5 |
|
27-Jul-2013 |
wenzelm <none@none> |
standardized aliases;
|
| #
02180a62 |
|
23-Jul-2013 |
krauss <none@none> |
eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates
--HG--
extra : source : daf022057a0d8c3cce0ca52d4d301b437fdf9553
|
| #
bb2fe771 |
|
28-Apr-2012 |
krauss <none@none> |
dependency graphs: fixed direction of edges
|
| #
55e11b0d |
|
03-Apr-2012 |
griff <none@none> |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
| #
ca981f61 |
|
14-Jan-2012 |
wenzelm <none@none> |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
| #
941cf8eb |
|
02-Dec-2011 |
wenzelm <none@none> |
more antiquotations;
|
| #
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
|
| #
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
| #
14d00fc2 |
|
12-Dec-2010 |
krauss <none@none> |
tuned headers
|
| #
d94c1a87 |
|
05-Oct-2010 |
krauss <none@none> |
discontinued continuations to simplify control flow; dropped optimization in scnp
|
| #
dbf9b53f |
|
05-Oct-2010 |
krauss <none@none> |
use Cache structure instead of passing tables around explicitly
|
| #
b11705e1 |
|
28-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix equality now named HOL.eq
|
| #
c91cbd4e |
|
27-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
| #
2275e3b0 |
|
19-Aug-2010 |
haftmann <none@none> |
more antiquotations
|
| #
bbda5041 |
|
19-Aug-2010 |
haftmann <none@none> |
use antiquotations for remaining unqualified constants in HOL
|
| #
53a0b22e |
|
01-Jul-2010 |
haftmann <none@none> |
"prod" and "sum" replace "*" and "+" respectively
|
| #
42aff2ea |
|
09-Jun-2010 |
haftmann <none@none> |
tuned quotes, antiquotations and whitespace
|
| #
07209de2 |
|
08-Jun-2010 |
haftmann <none@none> |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
| #
c3452482 |
|
06-Mar-2010 |
wenzelm <none@none> |
modernized structure Object_Logic;
|
| #
e3d0611a |
|
27-Feb-2010 |
wenzelm <none@none> |
modernized structure Term_Ord;
|
| #
e552e0c8 |
|
27-Feb-2010 |
wenzelm <none@none> |
just one copy of structure Term_Graph (in Pure);
|
| #
5e512ec7 |
|
27-Feb-2010 |
wenzelm <none@none> |
clarified @{const_name} vs. @{const_abbrev};
|
| #
75f69d99 |
|
10-Feb-2010 |
haftmann <none@none> |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
| #
7b3a0878 |
|
28-Jan-2010 |
haftmann <none@none> |
new theory Algebras.thy for generic algebraic structures
|
| #
a0dbfc4d |
|
03-Jan-2010 |
wenzelm <none@none> |
made SML/NJ happy;
|
| #
eb23531d |
|
02-Jan-2010 |
krauss <none@none> |
new year's resolution: reindented code in function package
|
| #
d9b94c22 |
|
02-Jan-2010 |
krauss <none@none> |
simplified
|
| #
15e88558 |
|
02-Jan-2010 |
krauss <none@none> |
absorb structures Decompose and Descent into Termination, to simplify further restructuring
|
| #
4678ef3f |
|
23-Nov-2009 |
krauss <none@none> |
eliminated dead code and some unused bindings, reported by polyml
|
| #
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|
| #
92ba9c59 |
|
18-Sep-2009 |
haftmann <none@none> |
inter and union are mere abbreviations for inf and sup
|
| #
d47cfa6f |
|
18-Sep-2009 |
haftmann <none@none> |
more antiquotations
|
| #
a4b600c4 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
| #
86fbc6fe |
|
22-Jul-2009 |
haftmann <none@none> |
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
|
| #
b063764f |
|
09-Jul-2009 |
wenzelm <none@none> |
renamed functor TableFun to Table, and GraphFun to Graph;
|
| #
d18d6a07 |
|
22-Jun-2009 |
haftmann <none@none> |
uniformly capitialized names for subdirectories
--HG--
rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML
rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML
rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML
rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML
rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML
rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML
rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML
rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML
rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML
rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML
rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML
rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML
rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML
rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML
rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML
rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML
rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML
rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML
rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML
rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML
rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML
rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML
rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML
rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML
rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML
rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML
rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML
rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML
rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML
rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML
rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML
rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML
rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML
rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML
|