Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/Rules/ROOT.ML
author blanchet
Mon, 19 Apr 2010 18:14:45 +0200
changeset 36230 43d10a494c91
parent 16546 77e7fd18b785
child 42637 381fdcab0f36
permissions -rw-r--r--
added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10341
6eb91805a012 added the $Id:$ line
paulson
parents: 10304
diff changeset 
     1
 
(* ID:         $Id$ *)
10304
a372910d82d6 part of set-up
paulson
parents:
diff changeset 
     2
 
use_thy "Basic";
a372910d82d6 part of set-up
paulson
parents:
diff changeset 
     3
 
use_thy "Blast";
a372910d82d6 part of set-up
paulson
parents:
diff changeset 
     4
 
use_thy "Force";
10847
b35a68ec8892 loads the new theory
paulson
parents: 10341
diff changeset 
     5
 
use_thy "Forward";
10956
1db8b894ada0 new examples theory Rules/Tacticals.thy
paulson
parents: 10847
diff changeset 
     6
 
use_thy "Tacticals";
10304
a372910d82d6 part of set-up
paulson
parents:
diff changeset 
     7
 







16546






77e7fd18b785
added find2



nipkow


parents: 
10956

diff
changeset




     8


use_thy "find2";














isabelle