Mercurial
Mercurial
>
repos
>
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
src/HOL/MiniML/Type.ML
1999-01-09
nipkow
Refined arith tactic.
file
|
diff
|
annotate
1998-11-27
nipkow
At last: linear arithmetic for nat!
file
|
diff
|
annotate
1998-09-21
oheimb
re-added mem and list_all
file
|
diff
|
annotate
1998-09-09
oheimb
reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
file
|
diff
|
annotate
1998-07-24
berghofe
Adapted to new datatype package.
file
|
diff
|
annotate
1998-07-03
nipkow
Removed leading !! in goals.
file
|
diff
|
annotate
1998-06-22
wenzelm
isatool fixgoal;
file
|
diff
|
annotate
1998-03-07
nipkow
Removed `addsplits [expand_if]'
file
|
diff
|
annotate
1997-12-30
nipkow
nth -> !
file
|
diff
|
annotate
1997-11-05
paulson
Ran expandshort, especially to introduce Safe_tac
file
|
diff
|
annotate
1997-11-03
wenzelm
isatool fixclasimp;
file
|
diff
|
annotate
1997-10-17
nipkow
setloop split_tac -> addsplits
file
|
diff
|
annotate
1997-10-16
nipkow
Simplified proof because of better simplifier.
file
|
diff
|
annotate
1997-10-10
wenzelm
fixed dots;
file
|
diff
|
annotate
1997-06-16
paulson
Type constraint added to ensure that "length" refers to lists. Maybe should
file
|
diff
|
annotate
1997-06-02
paulson
New statement and proof of free_tv_subst_var in order to cope with new
file
|
diff
|
annotate
1997-04-23
paulson
Ran expandshort
file
|
diff
|
annotate
1997-04-22
paulson
Ran expandshort
file
|
diff
|
annotate
1997-02-14
narasche
Some lemmas changed to valuesd
file
|
diff
|
annotate
1997-01-17
nipkow
The new version of MiniML including "let".
file
|
diff
|
annotate
1997-01-17
paulson
New miniscoping rules for the bounded quantifiers and UN/INT operators
file
|
diff
|
annotate
1996-09-26
paulson
Ran expandshort
file
|
diff
|
annotate
1996-08-08
berghofe
Removed unnecessary Addsimps.
file
|
diff
|
annotate
1996-05-20
nipkow
Added thm I_complete_wrt_W to I.
file
|
diff
|
annotate
1996-03-27
paulson
Now use _irrefl instead of _anti_refl
file
|
diff
|
annotate
1996-02-27
nipkow
used qed_spec_mp.
file
|
diff
|
annotate
1996-01-30
clasohm
expanded tabs
file
|
diff
|
annotate
1995-12-08
nipkow
Introduced Monad syntax Pat := Val; Cont
file
|
diff
|
annotate
1995-10-25
nipkow
New theory: type inference for let-free MiniML
file
|
diff
|
annotate
less
more
(0)
tip