Page MenuHomeIsabelle/Phabricator
Feed All Stories

Sun, May 31

traytel committed rAFPb5440f7e5a01: simplified Let constructor.
simplified Let constructor
Sun, May 31, 10:17 PM

Sat, May 30

florian.haftmann committed rISABELLE435cdc772110: specific atomization inert to later rule set modifications.
specific atomization inert to later rule set modifications
Sat, May 30, 8:07 PM
florian.haftmann committed rISABELLE3956d85e8e81: more precise scope of atomize.
more precise scope of atomize
Sat, May 30, 8:07 PM
florian.haftmann committed rISABELLE3867734b9a40: install simproc but deactivate by default.
install simproc but deactivate by default
Sat, May 30, 1:49 PM

Wed, May 27

makarius committed rISABELLE8357ee06ade1: adapted to d25093536482;.
adapted to d25093536482;
Wed, May 27, 10:00 PM
makarius committed rISABELLEb9fbc93f3a24: clarified markup;.
clarified markup;
Wed, May 27, 10:00 PM
makarius committed rISABELLEd25093536482: clarified signature;.
clarified signature;
Wed, May 27, 10:00 PM
makarius committed rISABELLEf8b0271cc744: tuned signature;.
tuned signature;
Wed, May 27, 10:00 PM
makarius updated the post content for Blog Post: Antiquotations for Isabelle systems programming.
Wed, May 27, 4:45 PM
makarius created Blog Post: Antiquotations for Isabelle systems programming.
Wed, May 27, 4:44 PM
makarius committed rISABELLEcdcf2fcf3f54: tuned;.
tuned;
Wed, May 27, 4:44 PM
makarius committed rISABELLEa63072d875d1: proper error positions;.
proper error positions;
Wed, May 27, 4:36 PM
makarius committed rISABELLE64c9628b39fc: more documentation on Isabelle/Scala;.
more documentation on Isabelle/Scala;
Wed, May 27, 4:36 PM
makarius committed rISABELLE0dc67ae4a4c7: more NEWS;.
more NEWS;
Wed, May 27, 4:36 PM
makarius committed rISABELLE70442ddbfb15: tuned whitespace;.
tuned whitespace;
Wed, May 27, 4:36 PM
makarius committed rISABELLE0da5fb75088a: more antiquotations;.
more antiquotations;
Wed, May 27, 4:36 PM
makarius committed rISABELLE1ca5623888bb: tuned;.
tuned;
Wed, May 27, 4:36 PM
makarius committed rISABELLE1529336eaedc: check bash functions against Isabelle settings environment;.
check bash functions against Isabelle settings environment;
Wed, May 27, 4:36 PM
makarius committed rISABELLE0408f6814224: misc tuning;.
misc tuning;
Wed, May 27, 4:36 PM
makarius committed rISABELLEf08cf9d8f90b: breakable scala_name;.
breakable scala_name;
Wed, May 27, 4:36 PM
makarius committed rISABELLE9a12eb655f67: tuned signature;.
tuned signature;
Wed, May 27, 4:35 PM
makarius committed rISABELLE2cf0b0293f0d: proper check of example;.
proper check of example;
Wed, May 27, 4:35 PM
makarius committed rISABELLE4df341249348: discontinued pointless document antiquotation;.
discontinued pointless document antiquotation;
Wed, May 27, 4:35 PM
makarius committed rISABELLEce06d6456cc8: clarified signature --- fit within limit of 22 arguments;.
clarified signature --- fit within limit of 22 arguments;
Wed, May 27, 4:35 PM
makarius committed rISABELLE7a39036d5a19: tuned;.
tuned;
Wed, May 27, 4:35 PM
makarius committed rISABELLEab21876c30c1: tuned;.
tuned;
Wed, May 27, 4:35 PM

Mon, May 25

makarius committed rISABELLEa27747c85700: more antiquotations;.
more antiquotations;
Mon, May 25, 11:03 PM
makarius committed rISABELLEdff81ce866d4: obsolete;.
obsolete;
Mon, May 25, 11:03 PM
makarius committed rISABELLE1b023a4498c3: check free-form Scala source;.
check free-form Scala source;
Mon, May 25, 11:03 PM
makarius committed rISABELLE3b35b0fd7fe8: clarified static_check: avoid accidental evaluation;.
clarified static_check: avoid accidental evaluation;
Mon, May 25, 11:03 PM
makarius committed rISABELLE8dbefe849666: omit pointless memoing: Scala compiler is rather bulky anyway;.
omit pointless memoing: Scala compiler is rather bulky anyway;
Mon, May 25, 11:03 PM
makarius committed rISABELLEfeb37a43ace6: clarified signature;.
clarified signature;
Mon, May 25, 11:03 PM
makarius committed rISABELLEf7d15620dd8e: antiquotations for Scala entities;.
antiquotations for Scala entities;
Mon, May 25, 11:03 PM
blanchette committed rAFP5a77ba9e257f: more systematic self-citations.
more systematic self-citations
Mon, May 25, 9:43 AM
florian.haftmann committed rISABELLE4f4695757980: better closeup and more consistent terminology.
better closeup and more consistent terminology
Mon, May 25, 7:45 AM

Sun, May 24

makarius committed rISABELLE45f85e283ce0: merged.
merged
Sun, May 24, 9:54 PM
makarius committed rISABELLE2bf0283fc975: proper stack_limit;.
proper stack_limit;
Sun, May 24, 9:54 PM
makarius committed rISABELLE44ba78056790: clarified signature;.
clarified signature;
Sun, May 24, 9:54 PM
makarius committed rISABELLE71de0a253842: proper check of registered Scala functions;.
proper check of registered Scala functions;
Sun, May 24, 9:54 PM
makarius committed rISABELLEf92c7e2ba8da: more accurate classpath for "isabelle scala";.
more accurate classpath for "isabelle scala";
Sun, May 24, 9:54 PM
makarius committed rISABELLE0ca353521753: asynchronous build_session: notably for Scala.fulfill protocol commands during….
asynchronous build_session: notably for Scala.fulfill protocol commands during…
Sun, May 24, 9:54 PM
makarius committed rISABELLEfe7ee970c425: clarified build_session protocol;.
clarified build_session protocol;
Sun, May 24, 9:54 PM
makarius committed rISABELLE3cd8449829fa: clarified signature;.
clarified signature;
Sun, May 24, 9:54 PM
makarius committed rISABELLEaaa984499d36: tuned signature;.
tuned signature;
Sun, May 24, 9:54 PM
makarius committed rISABELLEad063ac1f617: more robust: explicit check for PIDE session;.
more robust: explicit check for PIDE session;
Sun, May 24, 9:54 PM
makarius committed rISABELLEf5dd0abd49d1: clarified name;.
clarified name;
Sun, May 24, 9:54 PM
makarius committed rISABELLE9d31fe4ecaea: unused;.
unused;
Sun, May 24, 9:54 PM
makarius committed rISABELLEb5191ededb6c: check Scala source snippets from ML;.
check Scala source snippets from ML;
Sun, May 24, 9:54 PM
makarius committed rISABELLEa7b81dd9954e: tuned signature;.
tuned signature;
Sun, May 24, 9:54 PM
makarius committed rISABELLE82abfda58667: init default context;.
init default context;
Sun, May 24, 9:54 PM
makarius committed rISABELLE2b7840fb2f90: tuned message;.
tuned message;
Sun, May 24, 9:54 PM
makarius committed rISABELLE28def00726ca: more robust isabelle.Functions --- avoid Java reflection with unclear….
more robust isabelle.Functions --- avoid Java reflection with unclear…
Sun, May 24, 9:54 PM
makarius committed rISABELLE06ec50d9fc0a: clarified signature;.
clarified signature;
Sun, May 24, 9:54 PM
makarius committed rISABELLE3ee14fc25736: tuned;.
tuned;
Sun, May 24, 9:54 PM
makarius committed rISABELLE3882df6a4a93: tuned message;.
tuned message;
Sun, May 24, 9:54 PM
makarius committed rISABELLE081fdd53003a: more brackets (see 2e8af171887f);.
more brackets (see 2e8af171887f);
Sun, May 24, 9:54 PM
makarius committed rISABELLEbfc120aa737a: clarified signature;.
clarified signature;
Sun, May 24, 9:54 PM
makarius committed rISABELLEe95ea6956df3: unused;.
unused;
Sun, May 24, 9:54 PM
makarius committed rISABELLE8bbadb065ebe: more robust, notably for "isabelle scala";.
more robust, notably for "isabelle scala";
Sun, May 24, 9:54 PM
makarius committed rISABELLE1330fa4a2b85: clarified signature;.
clarified signature;
Sun, May 24, 9:54 PM
nipkow committed rISABELLE86cfb9fa3da8: reorganised sorted_set_of_list.
reorganised sorted_set_of_list
Sun, May 24, 10:46 AM
nipkow committed rISABELLE059d2cf529d4: merged.
merged
Sun, May 24, 10:46 AM
nipkow committed rISABELLE864fade05842: simpler inductions.
simpler inductions
Sun, May 24, 10:46 AM
paulson <lp15@cam.ac.uk> committed rISABELLEd73955442df5: a few new lemmas about functions.
a few new lemmas about functions
Sun, May 24, 12:01 AM

Sat, May 23

paulson <lp15@cam.ac.uk> committed rAFPda460a208d37: getting rid of inj_on_image_mem_iff_alt.
getting rid of inj_on_image_mem_iff_alt
Sat, May 23, 11:10 PM

Fri, May 22

nipkow committed rISABELLEe9df7895e331: comment makes no sense.
comment makes no sense
Fri, May 22, 7:22 PM
immler committed rAFPd798380a6ca7: no need to enforce safety of final interval enclosure.
no need to enforce safety of final interval enclosure
Fri, May 22, 3:24 PM
nipkow committed rAFP25ba40a59673: adapted to 3e343c0c2138.
adapted to 3e343c0c2138
Fri, May 22, 3:10 PM
nipkow committed rISABELLE3e343c0c2138: added simp lemma.
added simp lemma
Fri, May 22, 3:09 PM
immler committed rAFP47862306dbbd: recover from unsafe set during Picard iteration.
recover from unsafe set during Picard iteration
Fri, May 22, 12:37 PM
florian.haftmann committed rISABELLE6a51e64ba13d: slightly more specific implementations.
slightly more specific implementations
Fri, May 22, 6:29 AM
florian.haftmann committed rISABELLE30d92e668b52: tuned module name space for generated code.
tuned module name space for generated code
Fri, May 22, 6:29 AM

Thu, May 21

nipkow committed rISABELLE76784f47c60f: unused alias.
unused alias
Thu, May 21, 11:40 PM
paulson <lp15@cam.ac.uk> committed rAFP944409c54399: new theorems, esp. on order types.
new theorems, esp. on order types
Thu, May 21, 1:01 PM
florian.haftmann committed rISABELLE34ecb540a079: generalized and augmented.
generalized and augmented
Thu, May 21, 11:04 AM

Wed, May 20

makarius committed rISABELLEf640380aaf86: clarified signature;.
clarified signature;
Wed, May 20, 10:35 PM
makarius committed rISABELLE265bbad3d6af: clarified modules;.
clarified modules;
Wed, May 20, 10:35 PM
paulson <lp15@cam.ac.uk> committed rISABELLE3c7852327787: A few new theorems, plus some tidying up.
A few new theorems, plus some tidying up
Wed, May 20, 5:56 PM
florian.haftmann committed rISABELLEda12452c9be2: corrected spelling and tuned whitespace.
corrected spelling and tuned whitespace
Wed, May 20, 8:35 AM

Tue, May 19

makarius updated the post content for Blog Post: Release Candidates for Isabelle2020.
Tue, May 19, 5:38 PM
blanchette committed rAFPc6352b79465d: use lhd and lnull rather than lnth 0 and llength = 0 in IsaFoL.
use lhd and lnull rather than lnth 0 and llength = 0 in IsaFoL
Tue, May 19, 5:30 PM
blanchette committed rAFP12e81252fc8d: merged two files that used to be split for technical/political reasons.
merged two files that used to be split for technical/political reasons
Tue, May 19, 9:41 AM
blanchette committed rAFP00c6b844e775: more work on liminf llist library.
more work on liminf llist library
Tue, May 19, 9:34 AM
nipkow committed rISABELLE1a884605a08b: tuned.
tuned
Tue, May 19, 9:33 AM

Mon, May 18

makarius updated the post content for Blog Post: Update of Isabelle/Phabricator setup.
Mon, May 18, 5:08 PM
makarius created Blog Post: Update of Isabelle/Phabricator setup.
Mon, May 18, 5:08 PM
blanchette committed rAFP9df178c7dd08: enriched theorem proving library.
enriched theorem proving library
Mon, May 18, 5:07 PM
makarius committed rISABELLEb8d7b623e274: follow Phabricator update 2020 Week 19;.
follow Phabricator update 2020 Week 19;
Mon, May 18, 5:06 PM

Sun, May 17

nipkow committed rISABELLE57ace76cbffa: another AVL tree version.
another AVL tree version
Sun, May 17, 5:23 PM
kleing committed rAFP78e7e62b73bd: merge from afp-2020.
merge from afp-2020
Sun, May 17, 10:41 AM
kleing committed rAFP19fa00c4832d: adapt to Isabelle 07c85c68ff03.
adapt to Isabelle 07c85c68ff03
Sun, May 17, 10:41 AM
nipkow committed rAFP9a777766b777: New entry: Knuth_Bendix_Order.
New entry: Knuth_Bendix_Order
Sun, May 17, 10:41 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPbc386cdbebc6: sitegen.
sitegen
Sun, May 17, 10:41 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP91f85cde02c6: manual merge.
manual merge
Sun, May 17, 10:41 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPc5d1d917a936: changed metadata on request of Angeliki and Wenda.
changed metadata on request of Angeliki and Wenda
Sun, May 17, 10:41 AM
paulson <lp15@cam.ac.uk> committed rAFP728e00306996: Recursion-Addition.
Recursion-Addition
Sun, May 17, 10:41 AM
paulson <lp15@cam.ac.uk> committed rAFPa921275c45c0: sitegen for Recursion-Addition, plus fixed some typos in the abstract.
sitegen for Recursion-Addition, plus fixed some typos in the abstract
Sun, May 17, 10:41 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP5a8e71ddd499: new entry: Irrational_Series_Erdos_Straus.
new entry: Irrational_Series_Erdos_Straus
Sun, May 17, 10:41 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa74d8541a028: sitegen and metadata for Irrational_Series_Erdos_Straus.
sitegen and metadata for Irrational_Series_Erdos_Straus
Sun, May 17, 10:41 AM
nipkow committed rAFPc5aff697f6f2: lower case topics.
lower case topics
Sun, May 17, 10:41 AM