CJex hol-light issues - Githubissues

CJex / hol-light

HOL Light is an interactive theorem prover / proof checker. Automatically exported from code.google.com/p/hol-light

Other

1 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Examples/prog.ml: VC_TAC has trouble with with single-variable programs

#26 GoogleCodeExporter opened 9 years ago
0
Camlp5-6.12 is out

#25 GoogleCodeExporter opened 9 years ago
2
Documentation update from HOL4: GEN_REWRITE_TAC

#24 GoogleCodeExporter opened 9 years ago
1
Typos in documentation of 'injectivity' and 'distinctness'

#23 GoogleCodeExporter opened 9 years ago
1
Minor grammar issues in help

#22 GoogleCodeExporter opened 9 years ago
2
extra semicolon in SPECL's documentation

#21 GoogleCodeExporter opened 9 years ago
1
typo in PDF tutorial: double "a a"

#20 GoogleCodeExporter opened 9 years ago
1
minor issues with set_goal documentation

#19 GoogleCodeExporter opened 9 years ago
1
undocumented failure conditions of 'is_hidden'

#18 GoogleCodeExporter opened 9 years ago
1
link to undocumented entry in reference manual

#17 GoogleCodeExporter opened 9 years ago
1
typo in tutorial: "things" instead of "thinks" (page 90)

#16 GoogleCodeExporter opened 9 years ago
1
code examples in documentation contain extra space

#15 GoogleCodeExporter opened 9 years ago
1
extra punctuation after "i.e." in documentation

#14 GoogleCodeExporter opened 9 years ago
1
grammar error in 'new_type' documentation

#13 GoogleCodeExporter opened 9 years ago
1
string_of_term ignores the current line length

#12 GoogleCodeExporter opened 9 years ago
1
User pretty-printers don't print via the formatter argument

#11 GoogleCodeExporter opened 9 years ago
1
Conflicting definitions of - - ?

#10 GoogleCodeExporter opened 9 years ago
2
Problem building HOL light with OCaml 4

#9 GoogleCodeExporter opened 9 years ago
1
[PATCH] Fragile include for camlp4/camlp5

#8 GoogleCodeExporter opened 9 years ago
2
build fails with "cp: cannot stat `pa_j_3.1x_7.xx.ml': No such file or directory"

#7 GoogleCodeExporter opened 9 years ago
5
camlp5 version detection logic incorrect

#6 GoogleCodeExporter opened 9 years ago
6
hol-online link broken

#5 GoogleCodeExporter opened 9 years ago
2
Another error in pa_j.ml

#4 GoogleCodeExporter opened 9 years ago
1
Another error in pa_j.ml

#3 GoogleCodeExporter opened 9 years ago
7
Error in pa_j.ml with OCaml 3.12.0 and camlp5 6.02.2-2

#2 GoogleCodeExporter opened 9 years ago
11
pa_j.ml: parse error after upgrade to ocaml 3.12 and camlp5 6.02

#1 GoogleCodeExporter opened 9 years ago
11