| 1997-03-18 |
paulson |
1997-03-18 |
A more explicit prefix because gensym now generates easily predicatable
identifiers
|
file | diff | annotate |
| 1997-02-21 |
paulson |
1997-02-21 |
Replaced "flat" by the Basis Library function List.concat
|
file | diff | annotate |
| 1997-02-15 |
oheimb |
1997-02-15 |
added THEN_MAYBE and THEN_MAYBE'
|
file | diff | annotate |
| 1997-02-04 |
paulson |
1997-02-04 |
Gradual switching to Basis Library functions nth, drop, etc.
|
file | diff | annotate |
| 1996-11-27 |
paulson |
1996-11-27 |
Converted I/O operatios for Basis Library compatibility
|
file | diff | annotate |
| 1996-11-04 |
paulson |
1996-11-04 |
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
|
file | diff | annotate |
| 1996-09-23 |
paulson |
1996-09-23 |
Optimized version of SELECT_GOAL, up to 10% faster
|
file | diff | annotate |
| 1996-04-04 |
paulson |
1996-04-04 |
Fixed error in CHANGED (caused by variable renaming)
|
file | diff | annotate |
| 1996-03-15 |
paulson |
1996-03-15 |
Search tacticals moved to search.ML
|
file | diff | annotate |
| 1996-02-16 |
paulson |
1996-02-16 |
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
|
file | diff | annotate |
| 1996-01-29 |
clasohm |
1996-01-29 |
inserted tabs again
|
file | diff | annotate |
| 1996-01-29 |
clasohm |
1996-01-29 |
removed tabs
|
file | diff | annotate |
| 1995-03-03 |
clasohm |
1995-03-03 |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file | diff | annotate |
| 1994-11-22 |
lcp |
1994-11-22 |
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
Pure/tctical/DEPTH_FIRST: now suppresses duplicate solutions
|
file | diff | annotate |
| 1994-11-14 |
lcp |
1994-11-14 |
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
new SELECT_GOAL is MUCH faster
|
file | diff | annotate |
| 1994-11-11 |
lcp |
1994-11-11 |
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
REPEAT_DETERM_SOME: new
|
file | diff | annotate |
| 1994-10-31 |
lcp |
1994-10-31 |
Pure/tctical/THEN_ELSE: new
|
file | diff | annotate |
| 1994-10-12 |
lcp |
1994-10-12 |
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
next tactical call. There is no good way of doing this because of
backtracking.
Pure/tctical/exec_trace_command,tracify,traced_tac: these set, test and
reset suppress_tracing
|
file | diff | annotate |
| 1994-01-18 |
lcp |
1994-01-18 |
Many other files modified as follows:
s|Sign.cterm|cterm|g
s|Sign.ctyp|ctyp|g
s|Sign.rep_cterm|rep_cterm|g
s|Sign.rep_ctyp|rep_ctyp|g
s|Sign.pprint_cterm|pprint_cterm|g
s|Sign.pprint_ctyp|pprint_ctyp|g
s|Sign.string_of_cterm|string_of_cterm|g
s|Sign.string_of_ctyp|string_of_ctyp|g
s|Sign.term_of|term_of|g
s|Sign.typ_of|typ_of|g
s|Sign.read_cterm|read_cterm|g
s|Sign.read_insts|read_insts|g
s|Sign.cfun|cterm_fun|g
|
file | diff | annotate |
| 1993-10-21 |
lcp |
1993-10-21 |
Pure/drule/print_goals_ref: new, for Centaur interface
Pure/tctical/tracify,print_tac: now call !print_goals_ref
Pure/goals/print_top,prepare_proof: now call !print_goals_ref
|
file | diff | annotate |
| 1993-10-06 |
lcp |
1993-10-06 |
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
?'a from occurring -- which sometimes caused SELECT_GOAL to fail
|
file | diff | annotate |
| 1993-09-16 |
clasohm |
1993-09-16 |
Initial revision
|
file | diff | annotate |