Searched hist:9 (Results 1 - 25 of 3521) sorted by relevance
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ | ||
H A D | m1-story.acl2 | 9defa685 Tue Aug 17 01:42:10 MDT 2010 Matt Kaufmann <kaufmann@cs.utexas.edu> Updates to handle packages; also addition of jvm M1 model |
H A D | m1-story.lisp | 9defa685 Tue Aug 17 01:42:10 MDT 2010 Matt Kaufmann <kaufmann@cs.utexas.edu> Updates to handle packages; also addition of jvm M1 model |
H A D | pkg-test.acl2 | 9defa685 Tue Aug 17 01:42:10 MDT 2010 Matt Kaufmann <kaufmann@cs.utexas.edu> Updates to handle packages; also addition of jvm M1 model |
H A D | problem-set-1-answers.acl2 | 9defa685 Tue Aug 17 01:42:10 MDT 2010 Matt Kaufmann <kaufmann@cs.utexas.edu> Updates to handle packages; also addition of jvm M1 model |
H A D | problem-set-1-answers.lisp | 9defa685 Tue Aug 17 01:42:10 MDT 2010 Matt Kaufmann <kaufmann@cs.utexas.edu> Updates to handle packages; also addition of jvm M1 model |
/seL4-l4v-master/HOL4/examples/dev/AES/curried/ | ||
H A D | README | 9d480e6e Sun Jan 30 03:30:01 MST 2005 Konrad Slind <konrad.slind@gmail.com> Finally add same directory with different name. |
H A D | tablesScript.sml | 9d480e6e Sun Jan 30 03:30:01 MST 2005 Konrad Slind <konrad.slind@gmail.com> Finally add same directory with different name. |
/seL4-l4v-master/HOL4/Manual/LaTeX/ | ||
H A D | proof.sty | 9b8c83ad Mon Apr 22 08:27:00 MDT 2002 Michael Norrish <Michael.Norrish@nicta.com.au> A useful package for drawing inference trees. |
/seL4-l4v-master/HOL4/examples/RL_Environment/ | ||
H A D | RL_Lib.sml | 9bfd5cfe Fri Jul 27 13:19:41 MDT 2018 Ramana Kumar <ramana@member.fsf.org> Add some more tactics and make some tweaks |
/seL4-l4v-master/HOL4/examples/acl2/lisp/ | ||
H A D | check-file.lisp | 9d66e1e4 Wed Sep 08 03:47:23 MDT 2010 Matt Kaufmann <kaufmann@cs.utexas.edu> Added utility for checking round-trip output. |
/seL4-l4v-master/HOL4/help/Docfiles/ | ||
H A D | Drule.PART_MATCH_A.doc | 9d4c7968 Sun Sep 27 05:17:50 MDT 2015 Jeremy Dawson <jeremy@cecs.anu.edu.au> docs for PART_MATCH_A and REWR_CONV_A |
H A D | Parse.type_abbrev_pp.doc | 9f4b3059 Sat Nov 10 23:17:19 MST 2018 Michael Norrish <Michael.Norrish@nicta.com.au> Change type_abbrev to not alter printing behaviour If printing of abbreviations is desired, users must now use type_abbrev_pp. Closes #599 |
/seL4-l4v-master/HOL4/examples/machine-code/graph/seL4-kernel/ | ||
H A D | README | 9b3661d4 Thu Mar 14 01:41:00 MDT 2019 Magnus Myreen <myreen@chalmers.se> Tidy up RISC-V work on graph decompiler |
/seL4-l4v-master/HOL4/examples/machine-code/graph/seL4-kernel/riscv/ | ||
H A D | kernel-riscv.elf.txt | 9b3661d4 Thu Mar 14 01:41:00 MDT 2019 Magnus Myreen <myreen@chalmers.se> Tidy up RISC-V work on graph decompiler |
H A D | kernel-riscv.sigs | 9b3661d4 Thu Mar 14 01:41:00 MDT 2019 Magnus Myreen <myreen@chalmers.se> Tidy up RISC-V work on graph decompiler |
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/EXAMPLES/interactive/ | ||
H A D | insertionsort.sf | 9b0af68b Mon Feb 15 17:56:26 MST 2010 Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> insertion-sort example added |
/seL4-l4v-master/HOL4/src/opentheory/compat/ | ||
H A D | OpenTheoryRelationScript.sml | 9a27d2c2 Mon Nov 02 16:36:21 MST 2015 Ramana Kumar <ramana@member.fsf.org> start towards OpenTheory compatibility for relation and pred_set This is potentially going to be complicated since OpenTheory defines a type of sets and HOL4 does not. |
H A D | relationWriter.sml | 9a27d2c2 Mon Nov 02 16:36:21 MST 2015 Ramana Kumar <ramana@member.fsf.org> start towards OpenTheory compatibility for relation and pred_set This is potentially going to be complicated since OpenTheory defines a type of sets and HOL4 does not. |
/seL4-l4v-master/HOL4/src/parse/ | ||
H A D | GrammarAncestry.sig | 9e302fc8 Thu Sep 08 01:49:31 MDT 2016 Michael Norrish <Michael.Norrish@nicta.com.au> Track grammar ancestry in theory data. This ancestry is that set by the user; if the user says nothing then the ancestry will just be all of the theories loaded. |
/seL4-l4v-master/HOL4/src/q/ | ||
H A D | README | diff 9dd48c01 Wed Sep 16 11:13:32 MDT 2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk> Tuned. |
/seL4-l4v-master/HOL4/developers/ | ||
H A D | core-emacs-mode.sml | 9d21376a Tue Feb 26 19:37:28 MST 2019 Michael Norrish <Michael.Norrish@nicta.com.au> Provide stripped version of hol-mode.sml for developing pre hol.bare |
/seL4-l4v-master/HOL4/examples/acl2/ml/ | ||
H A D | kpa-v2-9-3.ml | 98bf3da6 Thu Jun 01 07:12:17 MDT 2006 Mike Gordon <mjcg@cl.cam.ac.uk> This file is generated from ACL2 (v2-9-3). It is in a form suitable for slurping into HOL and describes the package structure of the initial ACL2 system. |
/seL4-l4v-master/isabelle/src/Tools/jEdit/patches/ | ||
H A D | vfs_marker | 9f49196b Wed Jan 30 14:39:58 MST 2019 wenzelm <none@none> more accurate file position; |
/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ | ||
H A D | tptp_parser.ML | diff 9e8988bc Thu Aug 20 05:41:53 MDT 2015 wenzelm <none@none> precise BinIO, without newline conversion on Windows; |
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/patches/ | ||
H A D | vfs_marker | 9f49196b Wed Jan 30 14:39:58 MST 2019 wenzelm <none@none> more accurate file position; |
Completed in 278 milliseconds